Abstract
We show how by combining Explicit Model Checking techniques and simulation it is possible to effectively carry out (bounded) System Level Formal Verification of large Hybrid Systems such as those defined using model-based tools like Simulink.
We use an explicit model checker (namely, CMurphi) to generate all possible (finite horizon) simulation scenarios and then optimise the simulation of such scenarios by exploiting the ability of simulators to save and restore visited states. We show feasibility of our approach by presenting experimental results on the verification of the fuel control system example in the Simulink distribution. To the best of our knowledge this is the first time that (exhaustive) verification has been carried out for hybrid systems of such a size.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
Alur, R.: Formal verification of hybrid systems. In: Proc. EMSOFT 2011. ACM (2011)
Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P.: diVinE – A tool for distributed verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 278–281. Springer, Heidelberg (2006)
Bingham, B., Bingham, J., De Paula, F.M., Erickson, J., Singh, G., Reitblatt, M.: Industrial strength distributed explicit state model checking. In: Proc. PDMC-HIBI 2010. IEEE (2010)
Brillout, A., He, N., Mazzucchi, M., Kroening, D., Purandare, M., Rümmer, P., Weissenbacher, G.: Mutation-based test case generation for simulink models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 208–227. Springer, Heidelberg (2010)
Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005)
Cavaliere, F., Mari, F., Melatti, I., Minei, G., Salvo, I., Tronci, E., Verzino, G., Yushtein, Y.: Model checking satellite operational procedures. In: Proc. DASIA 2011 (2011)
De Paula, F.M., Hu, A.J.: An effective guidance strategy for abstraction-guided simulation. In: Proc. DAC 2007, pp. 63–68. ACM (2007)
Dean, J., Ghemawat, S.: Mapreduce: simplified data processing on large clusters. In: Proc. OSDI 2004. USENIX Association (2004)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.: Exploiting transition locality in automatic verification of finite state concurrent systems. STTT 6(4), 320–341 (2004)
Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol verification as a hardware design aid. In: Proc. IEEE Int. Conf. Comp. Design on VLSI in Comp. & Proc., 1991. IEEE (1992)
Gadkari, A.A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidhar, K.C.: AutoMOTGen: Automatic model oriented test generator for embedded control systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 204–208. Springer, Heidelberg (2008)
Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271–286. Springer, Heidelberg (2005)
Ho, P.H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal and simulation engines. In: Proc. ICCAD 2000 (2000)
Holzmann, G.J.: The SPIN model checker. Addison-Wesley (2003)
Holzmann, G.J.: Parallelizing the spin model checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 155–171. Springer, Heidelberg (2012)
Holzmann, G.J., Joshi, R., Groce, A.: Model driven code checking. Autom. Softw. Eng. 15(3-4), 283–297 (2008)
Kanade, A., Alur, R., Ivančić, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and analyzing symbolic traces of simulink/Stateflow models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 430–445. Springer, Heidelberg (2009)
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)
Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006)
Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in eddy. Int. J. Softw. Tools Technol. Transf. 11(1), 13–25 (2009)
Nanshi, K., Somenzi, F.: Guiding simulation with increasingly refined abstract traces. In: Proc. DAC 2006, pp. 737–742. ACM (2006)
Rozier, K.Y., Vardi, M.Y.: Deterministic compilation of temporal safety properties in explicit state model checking. In: Proc. HVC 2012. Springer (2012)
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Sontag, E.D.: Mathematical Control Theory: Deterministic Finite Dimensional Systems. Texts in Applied Mathematics. Springer (1998)
Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. Form. Methods Syst. Des. 18(2), 117–129 (2001)
Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Emb. Comp. Syst. 4(4), 779–818 (2005)
Tronci, E., Della Penna, G., Intrigila, B., Zilli, M.: A probabilistic approach to automatic verification of concurrent systems. In: Proc. APSEC 2001, pp. 317–324. IEEE (2001)
Venkatesh, R., Shrotri, U., Darke, P., Bokil, P.: Test generation for large automotive models. In: Proc. ICIT 2012, pp. 662–667. IEEE (2012)
Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 68–84. Springer, Heidelberg (2008)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. DAC 1998, pp. 599–604. ACM (1998)
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: Proc. HSCC 2010, pp. 243–252 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E. (2013). System Level Formal Verification via Model Checking Driven Simulation. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)