Model Checking

BTC Embedded Systems is clearly a pioneer when it comes to integrating model checking technology into commercial software tools. By making this highly automated technology accessible to the industry, we help our customers significantly increase the efficiency and quality of embedded development projects.

Model Checking – which should not be confounded with checking modeling guidelines in an environment like Simulink – originated in the early 1980s. The technique was originally invented by two research groups in the United States (Clark,Emmerson,McMillan) and France (Quielle/Sifakis). Both groups developed an efficient search procedure for finite state machines to determine whether they fulfill a specification expressed in temporal logic. This approach was later refined and optimized by introducing concepts like symbolic model checking or reduced ordered binary decision diagrams.

The purpose of a model checker is to extensively analyze the system behavior against a particular temporal property and automatically prove if this property holds. If it does not hold, the model checker returns a concrete counterexample explicitly showing how to violate the corresponding property. Contrary to testing, the model checker will analyze all possible runs of the system within one analysis task and deliver complete mathematical proof of the dynamic behavior of the system. The generation of a counterexample distinguishes model checking in particular from other automated analysis methods like abstract interpretation.

BTC EmbeddedPlatform combines different modeling checking techniques like Binary Decision Diagrams and SAT-Solvers. The appropriate method is selected automatically in an intelligent way according to the nature of the system-under-test. As an input and semantic foundation for the model checker, we use the ANSI-C production code, which makes the technology applicable for model-based development projects with automatically generated code as well as for handwritten code.

Model checking technology is used for various highly automated tasks within BTC EmbeddedPlatform. One application is the generation of structural test data for full code coverage within BTC EmbeddedTester. In this use case, model checking technology is not used to prove the absence of errors, but rather to generate test vectors by using "trap properties.” These would claim, for example, that some decision in an if-statement can never be fulfilled, i.e. belongs to dead code. When the model checker returns a counterexample, this indicates that the specific code part is not dead. The counterexample demonstrates how to fulfill the corresponding decision. Another use case is the Requirements-based Test Generation add-on for BTC EmbeddedTester BASE, which uses model checking to generate functional test cases from formalized requirements. Finally, BTC EmbeddedValidator applies the model checking technology to perform automated and complete mathematical proof that shows a particular requirement can never be violated by the system-under-test.