Abstract
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. © 2012 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Ferrante, O., Benvenuti, L., Mangeruca, L., Sofronis, C., & Ferrari, A. (2012). Parallel NuSMV: A NuSMV extension for the verification of complex embedded systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7613 LNCS, pp. 409–416). https://doi.org/10.1007/978-3-642-33675-1_38
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
