2015. cited By 4; Conference of 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015 ; Conference Date: 4 March 2015 Through 6 March 2015; Conference Code:118985

Paper doi abstract bibtex

Paper doi abstract bibtex

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation 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 assumeguarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model 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 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., in a private cluster), SyLVaaS allows full Intellectual Property protection on the SUV model and 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 industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution. © 2015 IEEE.

@CONFERENCE{Mancini2015476, author={Mancini, T. and Mari, F. and Massini, A. and Melatti, I. and Tronci, E.}, title={SyLVaaS: System level formal verification as a service}, journal={Proceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015}, year={2015}, pages={476-483}, doi={10.1109/PDP.2015.119}, art_number={7092763}, note={cited By 4; Conference of 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015 ; Conference Date: 4 March 2015 Through 6 March 2015; Conference Code:118985}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84962868623&partnerID=40&md5=c30948531aa1102eddf438e66c156ad8}, affiliation={Sapienza University of Rome, Italy}, abstract={The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation 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 assumeguarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model 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 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., in a private cluster), SyLVaaS allows full Intellectual Property protection on the SUV model and 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 industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution. © 2015 IEEE.}, keywords={Systems analysis; Traction (friction); Websites, Graceful degradation; Hardware in-the-loop simulation; Intellectual property protection; Operational environments; Parallel simulations; Platform independent; Verification activities; Verification problems, Formal verification}, references={Alur, R., Formal verification of hybrid systems (2011) Proc. EMSOFT 2011, pp. 273-278. , ACM; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proc. CAV 2013, Ser, 8044 LNCS, pp. 296-312. , Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proc. DSD 2014, , IEEE; System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proc. PDP 2014, , IEEE; Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M., Exploiting transition locality in automatic verification of finite state concurrent systems (2004) STTT, 6 (4), pp. 320-341; Ben-David, S., Grumberg, O., Heyman, T., Schuster, A., Scalable distributed on-the-fly symbolic model checking (2003) STTT, 4 (4), pp. 496-504; Kunkle, D., Slavici, V., Cooperman, G., Parallel disk-based computation for large, monolithic binary decision diagrams (2010) Proc. PASCO 2010, pp. 63-72. , ACM; Ábrahám, E., Schubert, T., Becker, B., Fränzle, M., Herde, C., Parallel sat solving in bounded model checking (2011) Journal of Language and Computation, 21 (1), pp. 5-21; Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G., Parallel and distributed model checking in Eddy (2009) STTT, 11 (1), pp. 13-25; Barnat, J., Brim, L., Ceska, M., Rockai, P., Divine: Parallel distributed model checker (2010) Proc. 9th Intl. Workshop on Parallel and Distributed Methods in Verification and 2nd Intl. Workshop on High Performance Computational Systems Biology, pp. 4-7; Schaefer, I., Sauer, T., Towards verification as a service (2012) Eternal Systems, Ser. Communications in Computer and Information Science, 255, pp. 16-24. , Springer; Bellettini, C., Camilli, M., Capra, L., Monga, M., Distributed CTL model checking in the cloud (2013) CoRR; Cabodi, G., Singh, S., (2012) Proc. FMCAD 2012, , IEEE; Verzino, G., Cavaliere, F., Mari, F., Melatti, I., Minei, G., Salvo, I., Yushtein, Y., Tronci, E., Model checking driven simulation of sat procedures (2012) Proc. SpaceOps 2012; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to Simulink/Stateflow verification (2010) Proc. HSCC 2010, pp. 243-252. , ACM; Tronci, E., Mancini, T., Salvo, I., Sinisi, S., Mari, F., Melatti, I., Massini, A., Ille, F., Patient-specific models from inter-patient biological models and clinical records (2014) Proc. FMCAD 2014, pp. 207-214. , FMCAD Inc; Mancini, T., Mari, F., Melatti, I., Salvo, I., Tronci, E., Gruber, J., Hayes, B., Elmegaard, L., Demand-aware price policy synthesis and verification services for smart grids (2014) Proc. SmartGridComm 2014, , IEEE; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) Proc. CAV 2005, Ser. LNCS, 3576, pp. 266-280. , Springer; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proc. APSEC 2001, pp. 317-324. , IEEE; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proc. TACAS 2005, Ser, 3440 LNCS, pp. 271-286. , Springer; Tripakis, S., Sofronis, C., Caspi, P., Curic, A., Translating discretetime Simulink to Lustre (2005) ACM Trans. Emb. Comp. Syst., 4 (4), pp. 779-818; Whalen, M., Cofer, D., Miller, S., Krogh, B., Storm, W., Integration of formal analysis into a model-based software development process (2007) Proc. FMICS 2007, pp. 68-84; Nanshi, K., Somenzi, F., Guiding simulation with increasingly refined abstract traces (2006) Proc. DAC 2006, pp. 737-742. , ACM; De Paula, F., Hu, A., An effective guidance strategy for abstraction-guided simulation (2007) Proc. DAC 2007, pp. 63-68. , ACM; Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P., Divine: A tool for distributed verification (2006) Proc. CAV 2006, pp. 278-281. , Springer; Holzmann, G., Parallelizing the SPIN model checker (2012) Proc. SPIN 2012, pp. 155-171. , Springer; Laarman, A., Van De Pol, J., Weber, M., Boosting multi-core reachability performance with shared hash tables (2010) Proc. FMCAD 2010, pp. 247-255. , IEEE; Mari, F., Melatti, I., Salvo, I., Tronci, E., Model based synthesis of control software from system level formal specifications (2014) ACM Trans. Softw. Eng. and Method., 23 (1); (2012) Theoretical Aspects of Computing - ICTAC 2012, Ser, 7521 LNCS, pp. 243-258. , Springer; Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E., On model based synthesis of embedded control software (2012) Proc. EMSOFT 2012, pp. 227-236. , ACM; Automatic control software synthesis for quantized discrete time hybrid systems (2012) Proc. CDC 2012, pp. 6120-6125. , IEEE; On-the-fly control software synthesis (2013) Proc. SPIN 2013, Ser, 7976 LNCS, pp. 61-80. , Springer; A map-reduce parallel approach to automatic synthesis of control software (2013) Proc. SPIN 2013, Ser, 7976 LNCS, pp. 43-60. , Springer; Mari, F., Melatti, I., Salvo, I., Tronci, E., Synthesis of quantized feedback control software for discrete time linear hybrid systems (2010) Proc. CAV 2010, Ser, 6174 LNCS, pp. 180-195. , Springer; Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M., Synchronized regular expressions (2003) Acta Inf., 39 (1), pp. 31-70; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, Ser. Texts in Applied Math, , Springer}, editor={Lilius J., Daneshtalab M., Brorsson M., Leppanen V., Aldinucci M.}, sponsors={}, publisher={Institute of Electrical and Electronics Engineers Inc.}, isbn={9781479984909}, language={English}, abbrev_source_title={Proc. - Euromicro Int. Conf. Parallel, Distributed, Netw.-Based Process., PDP}, document_type={Conference Paper}, source={Scopus}, }

Downloads: 0