Parallel NuSMV: A NuSMV Extension for the Verification of Complex Embedded Systems

  • Orlando Ferrante
  • Luca Benvenuti
  • Leonardo Mangeruca
  • Christos Sofronis
  • Alberto Ferrari
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7613)


In this paper we present Parallel NuSMV, a tool based on the NuSMV model checker that integrates the ManySAT parallel SAT solver. The PNuSMV is part of the FormalSpecs Verifier framework for the formal verification of Simulink/Stateflow models. The experiments we performed show that the use of a parallel SAT solver allows for an average speedup of an order of magnitude or more on industry-level size models. The main contributions of the papers are (1) the description of the PNuSMV model checker (2) the description of the verification time speedup w.r.t. the NuSMV tool for the verification of industrial-sized embedded systems and (3) the integration of the tool in the FormalSpecs Verifier framework for the verification of Simulink/Stateflow models with the application to a cruise control case study.


model checking embedded systems contract-based design formal verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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, pp. 15–18 (2005)Google Scholar
  2. 2.
    Miller, S., Whalen, M., Cofer, D.: Software model checking takes off. Communications of the ACM 53(2), 58–64 (2010)CrossRefGoogle Scholar
  3. 3.
    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. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
  5. 5.
  6. 6.
    Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with slamGoogle Scholar
  7. 7.
    Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Godefroid, P.: Compositional dynamic test generation (extended abstract)Google Scholar
  9. 9.
    Burch, J.R., Clarke, E.M., Mcmillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10 20 states and beyond (1990)Google Scholar
  10. 10.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  11. 11.
    Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, vol. 4 (2009)Google Scholar
  12. 12.
    Hamadi, Y., Sais, L.: Manysat: a parallel sat solver. Journal on Satisfiability, Boolean Modeling and Computation, JSAT (2009)Google Scholar
  13. 13.
  14. 14.
    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)Google Scholar
  15. 15.
    Een, N., Sörensson, N.: An extensible sat-solver (ver 1.2) (2003)Google Scholar
  16. 16.
    Herbstritt, M.: zchaff: Modifications and extensions (2001)Google Scholar
  17. 17.
    Murray, R.M., et al.: Feedback Systems An Introduction for Scientists and Engineers. Princenton University Press (2009)Google Scholar
  18. 18.
    Benvenuti, L., Ferrari, A., Mangeruca, L., Mazzi, E., Passerone, R., Sofronis, C.: A contract-based formalism for the specification of heterogeneous systems (invited). In: FDL, pp. 142–147. IEEE (2008)Google Scholar
  19. 19.
    Ferrante, O., Codella, G., Sofronis, C., Mangeruca, L., Ferrari, A.: Verify contract-based designed discrete systems by simulation. In: INCOSE, EuSEC (2010)Google Scholar
  20. 20.
    Ferrante, O., Mignogna, A., Sofronis, C., Mangeruca, L., Ferrari, A.: Contract based design chain integration: An automotive domain case study. In: Applied Simulation and Modelling. ACTA Press (2011)Google Scholar
  21. 21.

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Orlando Ferrante
    • 1
  • Luca Benvenuti
    • 1
  • Leonardo Mangeruca
    • 1
  • Christos Sofronis
    • 1
  • Alberto Ferrari
    • 1
  1. 1.ALES S.r.l.RomeItaly

Personalised recommendations