Parallel and Distributed Invariant Checking of Microcontroller Software

Formal verification techniques are recognized as promising tools for the development of embedded systems. One such technique is invariant checking, which can be applied intuitively by developers as it does not require knowledge of temporal logics. State spaces for invariant checking are built using the same methods as used for model checking. They can become large due to the state-explosion problem. In [mc]square, which is a model checker for microcontroller programs, most of the time is spent building state spaces when checking programs. To improve the performance of [mc]square, we have implemented four parallel and one distributed algorithm for invariant checking. Parallel algorithms are especially helpful as they allow to fully utilize multi-core CPUs. This paper describes several parallel and distributed algorithms and presents a case study that compares these algorithms and shows the performance improvements achieved.