One of the Holy Grails of computing has been proving the correctness of a program. Now MathWorks has incorporated a formal methods capability into its SimuLink tool. It is called Design Verifier. It generates tests for Simulink and Stateflow models that satisfy model coverage and user-defined objectives. It also proves model properties and generates examples of violations.
The technology is based on the Prover PlugIn proof engine from the Prover Technology AB.
No comments:
Post a Comment