San Diego — Adding formal design methods to its widely used Simulink model-based design suite, The Mathworks Inc. has introduced the Simulink Design Verifier, which generates tests and proves properties for models from the company's Simulink simulation platform and Stateflow design and simulation tool.
Design Verifier is based on the Prover Plug-In proof engine from formal verification provider Prover Technology AB. The Mathworks demonstrated the tool at the 44th Design Automation Conference here last week.
The company decided to add formal methods to existing design software to give developers of safety-critical applications adequate test coverage, said Ken Karnofsky, marketing director for signal processing and communications at The Mathworks (Natick, Mass.). The initial adopters will be embedded-software developers, Karnofsky said, but he believes the capability will appeal to both hardware and software designers in the long run.
Formal methods allow designers to “test and find errors that are very hard to catch by simulation alone,” said Paul Barnard, marketing director for design automation at The Mathworks. “You can do some kind of exhaustive simulation to try and catch every case, but formal methods do a better job of zeroing in on those cases earlier.”
What's needed, Barnard said, is a combination of formal methods and simulation.
The test generation capability in Design Verifier lets engineers obtain test cases to support industry-standard, safety-critical metrics, such as modified condition/decision coverage. Users can define custom test objectives directly in Simulink or Stateflow models by using design verification blocks. For example, a user could decide to generate only tests that provide 100 percent decision coverage.
The property-proving capability of Design Verifier lets users find such problems as missed requirements and unwanted states. Users can, for example, identify unachievable model coverage, such as states that cannot be entered, switch conditions that cannot occur and subsystems that cannot execute.
Users define properties on Simulink or Stateflow models to be always true or false, Barnard said. Though there technically are no limits as to complexity, the tool is intended to be used for a “reasonably sized component” of a model, not a model with thousands of blocks, he said.
Pass and fail
Design Verifier then provides a report showing which properties have passed and which have failed. For those that have failed, the tool generates counterexamples.
To generate tests with Design Verifier, users provide the model and specify the desired coverage and test objectives. In addition to test vectors, Design Verifier generates a test harness that includes test input values and expected outputs within a “signal builder” block. The same kind of test harness is generated for failed properties.
A verification subsystem block in the Design Verifier library lets users define complex proof objectives and constraints using Simulink and Stateflow constructs without affecting the simulation. Design Verifier functionality can be scripted and executed in batch mode from the Matlab environment.
Mathworks' Simulink Design Verifier is available now on Windows and Linux platforms starting at $8,000.