Experience report: Formal verification and testing in the development of embedded software

The paper summarizes our experiences in applying formal verification using the explicit-state model checker SPIN and combining it with a model-based testing approach to support the validation of embedded software. The discussed example covers a crucial part of the firmware of the fault-tolerant programmable logic controller Siemens SIMATIC S7-400H. The chosen approach is outlined and obstacles that were faced during the project are discussed. The paper advocates why formal verification is not suitable as a standalone method in industrial projects. Rather it must be combined with an appropriate validation method such as testing to maximize the benefits from the combination of both approaches. In this case, formal verification complements code or design model reviews, and testing benefits from the availability of correct formal models provided during verification process.