Formal Verification of Models and Code

12:45–13:30

Simulink is becoming a popular platform for system design by engineers worldwide. With the increase in complexity of engineering applications, there is a proportional increase in the complexity of models that depict the algorithm behaviour and thereby the software that implements these algorithms. Engineers rely on traditional techniques of model and code testing such as functional testing, unit testing, semantic checking, and analysis in simulation for uncovering overflow and underflow errors, dead logic, requirements testing, and assertion violations. These techniques may or may not uncover gaps in the design and are a function of how exhaustively the engineer has tested the design. In this session, we show how you can use Simulink Design Verifier™ and formal methods–based techniques to discover whether specific dynamic execution scenarios can occur and under what conditions. Using this information, you can then either improve the design and its requirements or guide the simulation for debugging and validation. In this session, you will also learn about how you can use the abstract interpretation techniques in Polyspace^® code verifiers to bridge the gap between conventional static analysis techniques and dynamic testing by verifying the dynamic properties of software applications at compilation time. Without executing the program itself, Polyspace products investigate all possible behaviours of a program execution, for each instruction, taking into account all possible values of every variable at every point in the code. The results provide conformance of source code to standards such as MISRA^®, detect run-time errors and prove their absence, and identify run-time errors when source code is modified.