NATICK, Mass.—(BUSINESS WIRE)—June 4, 2007— The MathWorks today introduced Simulink(R) Design Verifier, which generates tests and proves design properties for Simulink(R) and Stateflow(R) models using the Prover(R) Plug-In from Prover Technology.
Developers of embedded systems--especially complex or
safety-critical systems--can now automatically obtain test cases to
satisfy industry-standard metrics, such as modified condition/decision
coverage (MC/DC), while uncovering design errors earlier in the
development process when they are significantly less expensive to fix.
Simulation, a key activity of Model-Based Design, enables
engineers to gain insight into system behavior, tune parameters for
optimal performance, and ensure that their design behaves as intended.
Simulink Design Verifier augments simulation with new verification and
validation technology based on formal methods that significantly
reduces the need to hand-code tests for establishing complete model
coverage and verifying requirements.
Engineers can generate test inputs that satisfy standard coverage
objectives as well as user-defined test objectives and requirements.
These test inputs can also be combined with tests defined using
measured data so that simulations are testing against model coverage,
requirements, and real-world scenarios.
For property proving, engineers can directly capture design
requirements and performance objectives as properties in their
Simulink or Stateflow models. Simulink Design Verifier mathematically
proves whether those properties are satisfied and, if not, provides
counterexamples that would violate the properties. As a result,
engineers can find design flaws, unsatisfied requirements, and
unreachable states or logic that would be difficult to uncover using
"Model-Based Design is becoming widely used for embedded system
development, moving from R&D and proof-of-concept projects into
production programs," said Paul Barnard, marketing director of design
automation at The MathWorks. "With this shift, customers have a
critical need for verification, validation, and testing tools that
Simulink Design Verifier helps to address."
Simulink Design Verifier incorporates the Prover Plug-In proof
engine from Prover Technology, which automatically generates test
cases and counterexamples. It also performs proofs by using automated
mathematical reasoning to explore model execution paths. Such
systematic analysis complements simulation and provides deeper insight
into the behavior of designs.
"We worked closely with The MathWorks to extend our Prover Plug-In
interface to handle the dynamic systems that are typically modeled in
Simulink and Stateflow," said Marcus Tallhamn, chief marketing officer
at Prover Technology. "We are proud to be part of a tool that enables
embedded system developers without formal-methods expertise to perform
state-of-the-art formal verification."
Availability and Pricing
Simulink Design Verifier is available immediately for the
Microsoft Windows and Linux platforms. U.S. list prices start at
About The MathWorks
The MathWorks is the world's leading developer of technical
computing and Model-Based Design software for engineers and scientists
in industry, government, and education. With an extensive product set
based on MATLAB(R) and Simulink, The MathWorks provides software and
services to solve challenging problems and accelerate innovation in
automotive, aerospace, communications, financial services,
biotechnology, electronics, instrumentation, process, and other
The MathWorks was founded in 1984 and employs more than 1,600
people worldwide, with headquarters in Natick, Massachusetts. For
additional information, visit www.mathworks.com.
MATLAB, Simulink, Stateflow, Handle Graphics, Real-Time Workshop,
SimBiology, SimHydraulics, and xPC TargetBox are registered trademarks
and SimEvents is a trademark of The MathWorks, Inc. Prover, Prover
Technology, Prover Plug-In, and the Prover logo are trademarks or
registered trademarks of Prover Technology AB in Sweden, the United
States, and in other countries. Other product or brand names are
trademarks or registered trademarks of their respective holders.