On checking equivalence of simulation scripts. (English) Zbl 07363405

Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico

J. Log. Algebr. Methods Program. 120, Article ID 100640, 22 p. (2021).

Summary: To support Model Based Design of Cyber-Physical Systems (CPSs) many simulation based approaches to System Level Formal Verification (SLFV) have been devised. Basically, these are Bounded Model Checking approaches (since simulation horizon is of course bounded) relying on simulators to compute the system dynamics and thereby verify the given system properties. The main obstacle to simulation based SLFV is the large number of simulation scenarios to be considered and thus the huge amount of simulation time needed to complete the verification task. To save on computation time, simulation based SLFV approaches exploit the capability of simulators to save and restore simulation states. Essentially, such a time saving is obtained by optimising the simulation script defining the simulation activity needed to carry out the verification task. Although such approaches aim to (bounded) formal verification, as a matter of fact, the proof of correctness of the methods to optimise simulation scripts basically relies on an intuitive semantics for simulation scripting languages. This hampers the possibility of formally showing that the optimisations introduced to speed up the simulation activity do not actually omit checking of relevant behaviours for the system under verification. The aim of this paper is to fill the above gap by presenting an operational semantics for simulation scripting languages and by proving soundness and completeness properties for it. This, in turn, enables formal proofs of equivalence between unoptimised and optimised simulation scripts.

MSC:

68-XX

Computer science

Keywords:

formal verification; simulation based formal verification; formal verification of cyber-physical systems; system-level formal verification

Software:

AutoMOTGen; PHAVer; S-TaLiRo; Dymola; Uppaal; HyTech; StateFlow; DryVR; dReach

References:

[1]	RTCA DO-178C, Software Considerations in Airborne Systems and Equipment Certification, December 2011.
[2]	Alur, R., Formal verification of hybrid systems, (EMSOFT 2011 (2011), ACM)
[3]	Bengtsson, J.; Larsen, K.; Larsson, F.; Pettersson, P.; Yi, W., UPPAAL — a tool suite for automatic verification of real-time systems, (Hybrid Systems III. Hybrid Systems III, LNCS, vol. 1066 (1996), Springer)
[4]	Henzinger, T.; Ho, P.-H.; Wong-toi, H., HyTech: a model checker for hybrid systems, Int. J. Softw. Tools Technol. Transf., 1 (1997) · Zbl 1060.68603
[5]	Della Penna, G.; Intrigila, B.; Melatti, I.; Tronci, E.; Venturini Zilli, M., Exploiting transition locality in automatic verification of finite state concurrent systems, Int. J. Softw. Tools Technol. Transf., 6, 4 (2004)
[6]	Frehse, G., PHAVer: algorithmic verification of hybrid systems past hytech, Int. J. Softw. Tools Technol. Transf., 10, 3 (2008) · Zbl 1078.93533
[7]	Cimatti, A.; Roveri, M.; Susi, A.; Tonetta, S., Validation of requirements for hybrid systems: a formal approach, ACM Trans. Softw. Eng. Methodol., 21, 4 (2013)
[8]	Kong, S.; Gao, S.; Chen, W.; Clarke, E., dreach: δ-reachability analysis for hybrid systems, (TACAS 2015. TACAS 2015, LNCS, vol. 9035 (2015), Springer)
[9]	Simulink
[10]	VisSim
[11]	Modelica
[12]	OpenModelica
[13]	JModelica
[14]	Dymola
[15]	E. C. for Space Standardization (ECSS), System modelling and simulation, ESA Requirements and Standards Division, ECSS-E-TM-10-21A, 2010.
[16]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Merli, F.; Tronci, E., System level formal verification via model checking driven simulation, (CAV 2013. CAV 2013, LNCS, vol. 8044 (2013), Springer)
[17]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation, (DSD 2014 (2014), IEEE)
[18]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation, (PDP 2014 (2014), IEEE)
[19]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E., SyLVaaS: system level formal verification as a service, (PDP 2015 (2015), IEEE) · Zbl 1374.68294
[20]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E., Anytime system level verification via parallel random exhaustive hardware in the loop simulation, Microprocess. Microsyst., 41 (2016)
[21]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E., SyLVaaS: system level formal verification as a service, Fundam. Inform., 1-2 (2016) · Zbl 1374.68294
[22]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Salvo, I.; Tronci, E., On minimising the maximum expected verification time, Inf. Process. Lett., 122 (2017) · Zbl 1422.68164
[23]	Database of relevant traffic scenarios for highly automated vehicles
[24]	Flames: a powerful scenario database management system
[25]	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E., Simulator semantics for system level formal verification, EPTCS, 193 (2015)
[26]	Hamon, G.; Rushby, J., An operational semantics for stateflow, (Wermelinger, M.; Margaria-Steffen, T., Fundamental Approaches to Software Engineering (2004), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 229-243 · Zbl 1129.68445
[27]	Bouissou, O.; Chapoutot, A., An operational semantics for simulink’s simulation engine, (Proc. 13th ACM SIGPLAN/SIGBED Int. Conf. Languages, Compilers, Tools and Theory for Embedded Systems, LCTES ‘12 (2012), ACM: ACM New York, NY, USA), 129-138
[28]	Bouissou, O.; Chapoutot, A., An operational semantics for simulink’s simulation engine, SIGPLAN Not., 47, 5, 129-138 (2012)
[29]	Kågedal, D.; Fritzson, P., Generating a modelica compiler from natural semantics specifications, (Proceedings of the Summer Computer Simulation Conference (1998))
[30]	Foster, S.; Thiele, B.; Cavalcanti, A.; Woodcock, J., Towards a utp semantics for modelica, (Bowen, J.; Zhu, H., Unifying Theories of Programming (2017), Springer International Publishing: Springer International Publishing Cham), 44-64 · Zbl 1483.68053
[31]	Verzino, G.; Cavaliere, F.; Mari, F.; Melatti, I.; Minei, G.; Salvo, I.; Yushtein, Y.; Tronci, E., Model checking driven simulation of sat procedures, (SpaceOps 2012 (2012))
[32]	Bak, S.; Duggirala, P., Simulation-equivalent reachability of large linear systems with inputs, (CAV 2017. CAV 2017, LNCS, vol. 10426 (2017), Springer)
[33]	Fan, C.; Qi, B.; Mitra, S.; Viswanathan, M., DryVR: data-driven verification and compositional reasoning for automotive systems, (CAV 2017. CAV 2017, LNCS, vol. 10426 (2017), Springer)
[34]	Tripakis, S.; Sofronis, C.; Caspi, P.; Curic, A., Translating discrete-time Simulink to Lustre, ACM Trans. Embed. Comput. Syst., 4, 4 (2005)
[35]	Meenakshi, B.; Bhatnagar, A.; Roy, S., Tool for translating Simulink models into input language of a model checker, (ICFEM 2006 (2006), Springer)
[36]	Whalen, M.; Cofer, D.; Miller, S.; Krogh, B.; Storm, W., Integration of formal analysis into a model-based software development process, (FMICS 2007. FMICS 2007, LNCS, vol. 4916 (2007), Springer)
[37]	Annpureddy, Y.; Liu, C.; Fainekos, G. E.; Sankaranarayanan, S., S-TaLiRo: a tool for temporal logic falsification for hybrid systems, (TACAS 2011. TACAS 2011, LNCS, vol. 6605 (2011), Springer) · Zbl 1316.68069
[38]	Abbas, H.; Fainekos, G.; Sankaranarayanan, S.; Ivančić, F.; Gupta, A., Probabilistic temporal logic falsification of cyber-physical systems, ACM Trans. Embed. Comput. Syst., 12, 2s (2013)
[39]	Hoxha, B.; Dokhanchi, A.; Fainekos, G., Mining parametric temporal logic properties in model based design for cyber-physical systems, Int. J. Softw. Tools Technol. Transf. (2017)
[40]	Sankaranarayanan, S.; Kumar, S.; Cameron, F.; Bequette, B.; Fainekos, G.; Maahs, D., Model-based falsification of an artificial pancreas control system, ACM SIGBED Review, 14, 2 (2017)
[41]	Adimoolam, A.; Dang, T.; Donzé, A.; Kapinski, J.; Jin, X., Classification and coverage-based falsification for embedded control systems, (CAV 2017. CAV 2017, LNCS, vol. 10426 (2017), Springer)
[42]	Zuliani, P.; Platzer, A.; Clarke, E., Bayesian statistical model checking with application to Stateflow/Simulink verification, Form. Methods Syst. Des., 43, 2 (2013) · Zbl 1291.68273
[43]	Clarke, E.; Donzé, A.; Legay, A., On simulation-based probabilistic model checking of mixed-analog circuits, Form. Methods Syst. Des., 36, 2 (2010) · Zbl 1207.68205
[44]	Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L., Demand-aware price policy synthesis and verification services for smart grids, (SmartGridComm 2014 (2014), IEEE)
[45]	Hayes, B.; Melatti, I.; Mancini, T.; Prodanovic, M.; Tronci, E., Residential demand management using individualised demand aware price policies, IEEE Trans. Smart Grid, 8, 3 (2017)
[46]	Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L., User flexibility aware price policy synthesis for smart grids, (DSD 2015 (2015), IEEE)
[47]	Miskov-Zivanov, N.; Zuliani, P.; Clarke, E.; Faeder, J., Studies of biological networks with statistical model checking: application to immune system cells, (ACM-BCB 2013 (2013), ACM)
[48]	Tronci, E.; Mancini, T.; Salvo, I.; Sinisi, S.; Mari, F.; Melatti, I.; Massini, A.; Davi’, F.; Dierkes, T.; Ehrig, R.; Röblitz, S.; Leeners, B.; Krüger, T.; Egli, M.; Ille, F., Patient-specific models from inter-patient biological models and clinical records, (FMCAD 2014 (2014), IEEE)
[49]	Mancini, T.; Tronci, E.; Salvo, I.; Mari, F.; Massini, A.; Melatti, I., Computing biological model parameters by parallel statistical model checking, (IWBBIO 2015. IWBBIO 2015, LNCS, vol. 9044 (2015), Springer)
[50]	Broy, M.; Jonsson, B.; Katoen, J.; Leucker, M.; Pretschner, A., Model-Based Testing of Reactive Systems: Advanced Lectures (2005), Springer · Zbl 1070.68088
[51]	Gadkari, A.; Yeolekar, A.; Suresh, J.; Ramesh, S.; Mohalik, S.; Shashidhar, K., Automotgen: automatic model oriented test generator for embedded control systems, (CAV 2008. CAV 2008, LNCS, vol. 5123 (2008), Springer)
[52]	Kanade, A.; Alur, R.; Ivancic, F.; Ramesh, S.; Sankaranarayanan, S.; Shashidhar, K., Generating and analyzing symbolic traces of Simulink/Stateflow models, (CAV 2009. CAV 2009, LNCS, vol. 5643 (2009), Springer)
[53]	Brillout, A.; He, N.; Mazzucchi, M.; Kroening, D.; Purandare, M.; Rümmer, P.; Weissenbacher, G., Mutation-based test case generation for simulink models, (FMCO 2009 (2010), Springer)
[54]	Venkatesh, R.; Shrotri, U.; Darke, P.; Bokil, P., Test Generation for Large Automotive Models, ICIT 2012, vol. 7521 (2012), IEEE
[55]	Yang, C.; Dill, D., Validation with guided search of the state space, (DAC 1998 (1998), ACM)
[56]	Ho, P.; Shiple, T.; Harer, K.; Kukula, J.; Damiano, R.; Bertacco, V.; Taylor, J.; Long, J., Smart simulation using collaborative formal and simulation engines, (ICCAD 2000 (2000), IEEE)
[57]	Nanshi, K.; Somenzi, F., Guiding simulation with increasingly refined abstract traces, (DAC 2006 (2006), ACM)
[58]	De Paula, F.; Hu, A., An effective guidance strategy for abstraction-guided simulation, (DAC 2007 (2007), ACM)
[59]	Sontag, E., Mathematical Control Theory: Deterministic Finite Dimensional Systems (1998), Springer · Zbl 0945.93001
[60]	Cellier, F.; Kofman, E., Continuous System Simulation (2010), Springer
[61]	Kreisselmeier, G.; Birkholzer, T., Numerical nonlinear regulator design, IEEE Trans. Autom. Control, 39, 1 (1994) · Zbl 0796.93034
[62]	Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E., Automatic control software synthesis for quantized discrete time hybrid systems, (CDC 2012 (2012), IEEE)
[63]	Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E., Linearizing discrete-time hybrid systems, IEEE Trans. Autom. Control, 62, 10 (2017) · Zbl 1390.93322