SyLVaaS : System Level Formal Verification as a Service

• Autorzy: Mancini T. , Mari F. , Massini A. , Melatti I. , Tronci E.

Identyfikatory

DOI

10.3233/FI-2016-1444

• Konferencja: Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (22; 22.09.2015; Ferrara; Italy)
• Języki publikacji: EN

Abstrakty

EN

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variations in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to (Hardware In the Loop Simulation based) System Level Formal Verification. SyLVaaS takes as input a finite state automaton defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion (i.e., with no communication among the parallel processes) on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).

Słowa kluczowe

EN

verification as a service; model checking; hybrid systems; system level formal; verification; distributed multi-core hardware; loop simulation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 149, nr 1/2
• Strony: 101--132
• Opis fizyczny: Bibliogr. 63 poz., rys., tab., wykr.

Twórcy

autor

Mancini T.

• Computer Science Department, Sapienza University of Rome, Italy

autor

Mari F.

• Computer Science Department, Sapienza University of Rome, Italy

autor

Massini A.

• Computer Science Department, Sapienza University of Rome, Italy

autor

Melatti I.

• Computer Science Department, Sapienza University of Rome, Italy

autor

Tronci E.

• Computer Science Department, Sapienza University of Rome, Italy

Bibliografia

• [1] Mancini T, Mari F, Massini A, Melatti I, Tronci E. SyLVaaS: System Level Formal Verification as a Service. In: Proceedings of 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2015). IEEE; 2015. p. 476–483.
• [2] Alur R. Formal Verification of Hybrid Systems. In: Proceedings of 11th International Conference on Embedded Software (EMSOFT 2011). ACM; 2011. p. 273–278. doi:10.1145/2038642.2038685.
• [3] Mancini T, Mari F, Massini A, Melatti I, Merli F, Tronci E. System Level Formal Verification via Model Checking Driven Simulation. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV 2013). vol. 8044 of Lecture Notes in Computer Science. Springer; 2013. p. 296–312. doi:10.1007/978-3-642-39799-8_21.
• [4] Mancini T, Mari F, Massini A, Melatti I, Tronci E. Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation. In: Proceedings of 17th Euromicro Conference on Digital System Design (DSD 2014). IEEE; 2014. p. 236–245.
• [5] Mancini T, Mari F, Massini A, Melatti I, Tronci E. System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation. In: Proceedings of 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2014). IEEE; 2014. p. 734–742. doi:10.1109/PDP.2014.32.
• [6] Mancini T, Mari F, Massini A, Melatti I, Tronci E. Anytime System Level Verification via Parallel Random Exhaustive Hardware in the Loop Simulation. Microprocessors and Microsystems. 2016;41:12–28. doi:10.1016/j.micpro.2015.10.010.
• [7] Della Penna G, Intrigila B, Melatti I, Tronci E, Venturini Zilli M. Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems. International Journal on Software Tools for Technology Transfer. 2004;6(4):320–341. doi:10.1007/s10009-004-0149-6.
• [8] Sontag ED. Mathematical Control Theory: Deterministic Finite Dimensional Systems (2nd Ed.). Springer; 1998.
• [9] Clarke EM, Donzé A, Legay A. On Simulation-Based Probabilistic Model Checking of Mixed-Analog Circuits. Formal Methods in System Design. 2010;36(2):97–113. doi:10.1007/s10703-009-0076-y.
• [10] Zuliani P, Platzer A, Clarke EM. Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification. Formal Methods in System Design. 2013;43(2):338–367. doi:10.1007/s10703-013-0195-3.
• [11] Kim YJ, Kim M. Hybrid Statistical Model Checking Technique for Reliable Safety Critical Systems. In:Proceedings of 23rd IEEE International Symposium on Software Reliability Engineering. IEEE; 2012. p. 51–60.
• [12] Kim YJ, Choi O, Kim M, Baik J, Kim TH. Validating Software Reliability Early through Statistical Model Checking. IEEE Software. 2013;30(3):35–41. doi:10.1109/MS.2013.24.
• [13] Schrammel P, Kroening D, Brain M, Martins R, Teige T, Bienmüller T. Incremental Bounded Model Checking for Embedded Software (Extended Version). CoRR. 2014;abs/1409.5872.
• [14] Phillips JC, Sun Y, Jain N, Bohm EJ, Kalé LV. Mapping to Irregular Torus Topologies and Other Techniques for Petascale Biomolecular Simulation. In: Proceedings of International Conference for High Performance Computing, Networking, Storage and Analysis (SC 2014). IEEE; 2014. p. 81–91.
• [15] Schaefer I, Sauer T. Towards Verification as a Service. In: Eternal Systems. vol. 255 of Communications in Computer and Information Science. Springer; 2012. p. 16–24. doi:10.1007/978-3-642-28033-7_2.
• [16] Bellettini C, Camilli M, Capra L, Monga M. Distributed CTL Model Checking in the Cloud. CoRR. 2013;abs/1310.6670.
• [17] Verzino G, Cavaliere F, Mari F, Melatti I, Minei G, Salvo I, et al. Model Checking Driven Simulation of Sat Procedures. In: 12th International Conference on Space Operations (SpaceOps 2012); 2012. doi:10.2514/6.2012-1275611.
• [18] Tripakis S, Sofronis C, Caspi P, Curic A. Translating Discrete-Time Simulink to Lustre. ACM Transactions on Embedded Computing Systems. 2005;4(4):779–818. doi:10.1145/1113830.1113834.
• [19] Meenakshi B, Bhatnagar A, Roy S. Tool for Translating Simulink Models into Input Language of a Model Checker. In: Proceedings of 8th International Conference on Formal Engineering Methods (ICFEM 2006). Springer; 2006. p. 606–620. doi:10.1007/11901433_33.
• [20] Whalen MW, Cofer DD, Miller SP, Krogh BH, Storm W. Integration of Formal Analysis into a Model-Based Software Development Process. In: Proceedings of 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007). vol. 4916 of Lecture Notes in Computer Science. Springer; 2007. p. 68–84. doi:10.1007/978-3-540-79707-4_7.
• [21] Abbas H, Fainekos G, Sankaranarayanan S, Ivančić F, Gupta A. Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems. 2013;12(2s):95:1–95:30. doi:10.1145/2465787.2465797.
• [22] Zutshi A, Sankaranarayanan S, Deshmukh JV, Jin X. Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software. In: Proceedings of 19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2016). ACM; 2016. p. 135–144.
• [23] Duggirala PS, Mitra S, Viswanathan M, Potok M. C2E2: A Verification Tool for State flow Models. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). vol. 9035 of Lecture Notes in Computer Science. Springer; 2015. p. 68–82. doi:10.1007/978-3-662-46681-0_5.
• [24] Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W. UPPAAL—A Tool Suite for Automatic Verification of Real-Time Systems. In: Proceedings of Hybrid Systems III: Verification and Control. vol. 1066 of Lecture Notes in Computer Science. Springer; 1996. p. 232–243. doi:10.1007/BFb0020949.
• [25] Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, et al. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science. 1995;138(1):3–34. doi:10.1016/0304-3975(94)00202-T.
• [26] Henzinger TA, Ho PH, Wong-toi H. HyTech: A Model Checker for Hybrid Systems. International Journal on Software Tools for Technology Transfer. 1997;1:460–463.
• [27] Frehse G. PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. International Journal on Software Tools for Technology Transfer. 2008;10(3):263–279. doi:10.1007/s10009-007-0062-x.
• [28] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, et al. SpaceEx: Scalable Verification of Hybrid Systems. In: Proceedings of 23rd International Conference on Computer Aided Verification (CAV 2011). vol. 6806 of Lecture Notes in Computer Science. Springer; 2011. p. 379–395.
• [29] Cimatti A, Mover S, Tonetta S. SMT-Based Scenario Verification for Hybrid Systems. Formal Methods in System Design. 2013;42(1):46–66. doi:10.1007/s10703-012-0158-0.
• [30] Cimatti A, Griggio A, Mover S, Tonetta S. HyComp: An SMT-Based Model Checker for Hybrid Systems. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). vol. 9035 of Lecture Notes in Computer Science. Springer; 2015. p. 52–67. doi:10.1007/978-3-662-46681-0_4.
• [31] Bak S, Bogomolov S, Henzinger TA, Johnson TT, Prakash P. Scalable Static Hybridization Methods for Analysis of Nonlinear Systems. In: Proceedings of 19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2016). ACM; 2016. p. 155–164. doi:10.1145/2883817.2883837.
• [32] Cimatti A, Roveri M, Tonetta S. HRELTL. Information and Computation. 2015;245(C):54–71. doi:10.1016/j.ic.2015.06.006.
• [33] Sen K, Viswanathan M, Agha G. On Statistical Model Checking of Stochastic Systems. In: Proceedings of 17th International Conference on Computer Aided Verification (CAV 2005). vol. 3576 of Lecture Notes in Computer Science. Springer; 2005. p. 266–280.
• [34] Grosu R, Smolka SA. Monte Carlo Model Checking. In: Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005). vol. 3440 of Lecture Notes in Computer Science. Springer; 2005. p. 271–286. doi:10.1007/978-3-540-31980-1_18.
• [35] Tronci E, Della Penna G, Intrigila B, Venturini Zilli M. A Probabilistic Approach to Automatic Verification of Concurrent Systems. In: Proceedings of 8th Asia-Pacific Software Engineering Conference (APSEC 2001). IEEE; 2001. p. 317–324. doi:10.1109/APSEC.2001.991495.
• [36] Sivaraj H, Gopalakrishnan G. Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking. Electronic Notes in Theoretical Computer Science. 2003;89(1):51–67. doi:10.1016/S1571-0661(05)80096-9.
• [37] Della Penna G, Intrigila B, Melatti I, Tronci E, Venturini Zilli M. Finite Horizon Analysis of Markov Chains with the Murphi Verifier. International Journal on Software Tools for Technology Transfer. 2006;8(4–5):397–409. doi:10.1007/s10009-005-0216-7.
• [38] Jansen DN, Katoen JP, Oldenkamp M, Stoelinga MIA, Zapreev IS. How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In: Proceedings of Hardware and Software: Verification and Testing, 3rd International Haifa Verification Conference (HVC 2007). vol. 4899 of Lecture Notes in Computer Science. Springer; 2008. p. 69–85.
• [39] Younes HLS, Simmons RG. Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. In: Proceedings of 14th International Conference on Computer Aided Verification (CAV 2002). vol. 2404 of Lecture Notes in Computer Science. Springer; 2002. p. 223–235. doi:10.1007/3-540-45657-0_17.
• [40] Younes HLS. Ymer: A Statistical Model Checker. In: Proceedings of 17th International Conference on Computer Aided Verification (CAV 2005). vol. 3576 of Lecture Notes in Computer Science. Springer; 2005. p. 429–433. doi:10.1007/11513988_43.
• [41] Younes HLS. Probabilistic Verification for “Black-Box” Systems. In: Proceedings of 17th International Conference on Computer Aided Verification (CAV 2005). vol. 3576 of Lecture Notes in Computer Science. Springer; 2005. p. 253–265. doi:10.1007/11513988_25.
• [42] Younes HLS, Kwiatkowska MZ, Norman G, Parker D. Numerical vs. Statistical Probabilistic Model Checking. International Journal on Software Tools for Technology Transfer. 2006;8(3):216–228. doi:10.1007/s10009-005-0187-8.
• [43] David A, Larsen KG, Legay A, Mikučionis M, Wang Z. Time for Statistical Model Checking of Real-Time Systems. In: Proceedings of 23rd International Conference on Computer Aided Verification (CAV 2011). vol. 6806 of Lecture Notes in Computer Science. Springer; 2011. p. 349–355.
• [44] Tronci E, Mancini T, Salvo I, Sinisi S, Mari F, Melatti I, et al. Patient-Specific Models from Inter-Patient Biological Models and Clinical Records. In: Proceedings of 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2014). IEEE; 2014. p. 207–214.
• [45] Mancini T, Mari F, Melatti I, Salvo I, Tronci E, Gruber J, et al. Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids. In: Proceedings of 2014 IEEE International Conference on Smart Grid Communications (SmartGridComm 2014). IEEE; 2014. p. 794–799.
• [46] Yang CH, Dill DL. Validation with Guided Search of the State Space. In: Proceedings of 35th Conference on Design Automation (DAC 1998). ACM; 1998. p. 599–604. doi:10.1145/277044.277201.
• [47] Ho PH, Shiple T, Harer K, Kukula J, Damiano R, Bertacco V, et al. Smart Simulation using Collaborative Formal and Simulation Engines. In: Proceedings of 2000 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2000). IEEE; 2000. p. 120–126.
• [48] Nanshi K, Somenzi F. Guiding Simulation with Increasingly Refined Abstract Traces. In: Proceedings of 43rd Conference on Design Automation (DAC 2006). ACM; 2006. p. 737–742. doi:10.1145/1146909.1147097.
• [49] De Paula FM, Hu AJ. An Effective Guidance Strategy for Abstraction-Guided Simulation. In: Proceedings of 44th Conference on Design Automation (DAC 2007). ACM; 2007. p. 63–68. doi:10.1145/1278480.1278498.
• [50] Mari F, Melatti I, Salvo I, Tronci E. Model Based Synthesis of Control Software from System Level Formal Specifications. ACM Transactions on Software Engineering and Methodology. 2014;23(1):1–42.
• [51] Mari F, Melatti I, Salvo I, Tronci E. Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems. In: Proceedings of 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012). vol. 7521 of Lecture Notes in Computer Science. Springer; 2012. p. 243–258. doi:10.1007/978-3-642-32943-2_19.
• [52] Alimguzhin V, Mari F, Melatti I, Salvo I, Tronci E. On Model Based Synthesis of Embedded Control Software. In: Proceedings of 12th International Conference on Embedded Software (EMSOFT 2012). ACM; 2012. p. 227–236. doi:10.1145/2380356.2380398.
• [53] Alimguzhin V, Mari F, Melatti I, Salvo I, Tronci E. Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems. In: Proceedings of 51th IEEE Conference on Decision and Control (CDC 2012). IEEE; 2012. p. 6120–6125. doi:10.1109/CDC.2012.6426260.
• [54] Alimguzhin V, Mari F, Melatti I, Salvo I, Tronci E. On-the-Fly Control Software Synthesis. In: Proceedings of 20th International SPIN Symposium on Model Checking of Software (SPIN 2013). vol. 7976 of Lecture Notes in Computer Science. Springer; 2013. p. 61–80. doi:10.1007/978-3-642-39176-7_5.
• [55] Alimguzhin V, Mari F, Melatti I, Salvo I, Tronci E. A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software. In: Proceedings of 20th International SPIN Symposium on Model Checking of Software (SPIN 2013). vol. 7976 of Lecture Notes in Computer Science. Springer; 2013. p. 43–60. doi:10.1007/978-3-642-39176-7_4.
• [56] Mari F, Melatti I, Salvo I, Tronci E. Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems. In: Proceedings of 22nd International Conference on Computer Aided Verification (CAV 2010). vol. 6174 of Lecture Notes in Computer Science. Springer; 2010. p. 180–195. doi:10.1007/978-3-642-14295-6_20.
• [57] Della Penna G, Intrigila B, Tronci E, Venturini Zilli M. Synchronized Regular Expressions. Acta Informatica. 2003;39(1):31–70.
• [58] Stern U, Dill DL. Parallelizing the Murphi Verifier. Formal Methods in System Design. 2001;18(2):117–129. doi:10.1023/A:1008771324652.
• [59] Barnat J, Brim L, Černá I, Moravec P, Ročkai P, Šimeček P. DiVinE: a Tool for Distributed Verification. In: Proceedings of 18th International Conference on Computer Aided Verification (CAV 2006). vol. 4144 of Lecture Notes in Computer Science. Springer; 2006. p. 278–281. doi:10.1007/11817963_26.
• [60] Melatti I, Palmer R, Sawaya G, Yang Y, Kirby RM, Gopalakrishnan G. Parallel and Distributed Model Checking in Eddy. International Journal on Software Tools for Technology Transfer. 2009;11(1):13–25. doi:10.1007/s10009-008-0094-x.
• [61] Bingham B, Bingham J, De Paula FM, Erickson J, Singh G, Reitblatt M. Industrial Strength Distributed Explicit State Model Checking. In: Proceedings of 9th International Workshop on Parallel and Distributed Methods in Verification and 2nd International Workshop on High Performance Computational Systems Biology (PDMC-HIBI 2010). IEEE; 2010. p. 28–36. doi:10.1109/PDMC-HiBi.2010.13.
• [62] Laarman A, van de Pol J, Weber M. Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010). IEEE; 2010. p. 247–255.
• [63] Holzmann GJ. Parallelizing the SPIN Model Checker. In: Proceedings of 19th International SPIN Symposium on Model Checking of Software (SPIN 2012). vol. 7385 of Lecture Notes in Computer Science. Springer; 2012. p. 155–171. doi:10.1007/978-3-642-31759-0_12.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).