Simulink Design Verifier 2.0
Simulink requirement models
Mathworks's Simulink Design Verifier 2.0 (Fig. 1) incorporates static code analysis technology that is obtained when it acquired Polyspace Technologies. The Polyspace code verifiers detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access and other run-time errors. It also detects dead code. Polyspace was initially available for C/C++ and Ada source code.
Now this technology has been applied to Simulink graphical programming environment. The new tool checks blocks in a Simulink model. Blocks with errors are addressed in more detail with the tool calculating signal-range boundaries and generating test vectors that reproduce the error in simulation. The generated test vectors provide simulation inputs exercise the application model. This type of software-in-the-loop (SIL) and processor-in-the-loop (PIL) test configurations can significantly reduce errors in the final application.
The latest technology handles Simulink's fixed-point and floating point model support. Simulink can now check for assertion violations.
The functional requirements can be specified using a range of methods including Simulink models (Fig. 2), Matlab functions, and Stateflow definitions. The Simulink Design Verifier provides a variety of reports that highlight requirements that are met or violated. The system also provides model coverage analysis as well. This applies to Simulink and Stateflow models.
Text-based static analysis has proven invaluable allowing developers to identify errors even before an application is run. The Mathworks's Simulink Design Verifier expands this technology to the graphical programming space where the need is just as critical.