An application of parallel satisfiability solving to the verification of complex embedded systems

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.