Abstract
Model checking has reached a maturity level that allows its techniques to be applied to the verification of industrial systems. Several algorithms and methods have been proposed to increase its effectiveness to tackle models of increasing complexity. In this chapter we present an application of Parallel Satisfiability Solving to the verification of embedded control systems. The adopted toolchain is part of the Formal Specs Verifier framework for the formal verification of Simulink/Stateflow models. The experiments we performed show that the use of a parallel satisfiability solver allows for an average speedup of an order of magnitude or more on industrial strength models.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Miller, S., Anderson, E., Wagner, L., Whalen, M., Heimdahl, M.: Formal verification of flight critical software. In: Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit. (2005) 15–18
Miller, S., Whalen, M., Cofer, D.: Software model checking takes off. Communications of the ACM 53(2) (2010) 58–64
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. (2002) 359–364
Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM, Communications of the ACM, 54(7), pp 68–76, 2011.
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. pp 1–20, IFM, 2004.
Godefroid, P.: Compositional dynamic test generation (extended abstract), POPL 2007.
Burch, J.R., Clarke, E.M., Mc Millan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10ˆ20 states and beyond, LICS, 1990.
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (1999) 193–207
Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. Handbook of Satisfiability 4 (2009)
Hamadi, Y., Sais, L.: ManySAT: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) (2009)
Ferrari, A., Mangeruca, L., Ferrante, O., Mignogna, A.: DesyreML: a SysML profile for heterogeneous embedded systems. In: Embedded Real Time Software and Systems (ERTS). (2012)
Mangeruca, L., Ferrante, O., Ferrari, A.: Formalization and completeness of evolving requirements using contracts. In: 8th IEEE International Symposium on Industrial Embedded Systems (SIES). (2013)
Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Petrone, I., Velardi, L.: Contract-based analysis for verification of communication-based train control (CBTC) system. In: SAFECOMP. (2014)
Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Petrone, I., Velardi, L.: Contract modeling and verification with formal specs verifier toolsuite - application to Ansaldo STS rapid transit metro system use case. In: SAFECOMP. (2015)
Ferrante, O., Benvenuti, L., Mangeruca, L., Sofronis, C., Ferrari, A.: Parallel NuSMV: a NuSMV extension for the verification of complex embedded systems. Lecture Notes in Computer Science: Computer Safety, Reliability, and Security 7613 (2012) 409–416
Marazza, M., Ferrante, O., Ferrari, A.: Automatic generation of failure scenarios for sytems-on-chip. In: Real Time Software and Systems (ERTS). (2014)
Ferrante, O., Ferrari, A., Marazza, M.: An algorithm for the incremental generation of high coverage test suites. In: 19th IEEE European Test Symposium. (2014)
Ferrante, O., Ferrari, A., Marazza, M.: Formal Specs Verifier ATG: a tool for model-based generation of high coverage test suites. In: ERTS. (2016)
Een, N., Sörensson, N.: An extensible SAT-solver [ver 1.2] (2003)
Herbstritt, M.: zChaff: Modifications and extensions. (2001)
Murray, R.M., et al.: Feedback Systems An Introduction for Scientists and Engineers. Princeton University Press (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Ferrante, O., Ferrari, A., Sofronis, C., Mangeruca, L., Benvenuti, L. (2018). An Application of Parallel Satisfiability Solving to the Verification of Complex Embedded Systems. In: Hamadi, Y., Sais, L. (eds) Handbook of Parallel Constraint Reasoning. Springer, Cham. https://doi.org/10.1007/978-3-319-63516-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-63516-3_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63515-6
Online ISBN: 978-3-319-63516-3
eBook Packages: Computer ScienceComputer Science (R0)