Simulink
®
Design Verifier™
Release Notes
How to Contact The MathWorks
www.mathworks.
comp.soft-sys.matlab Newsgroup
www.mathworks.com/contact_TS.html Technical Support
suggest@mathworks.com Product enhancement suggestions
bugs@mathwo
doc@mathworks.com Documentation error reports
service@mathworks.com Order status, license renewals, passcodes
info@mathwo
com
rks.com
rks.com
Web
Bug reports
Sales, prici
ng, and general information
508-647-7000 (Phone)
508-647-7001 (Fax)
The MathWorks, Inc.
3 Apple Hill Drive
Natick, MA 01760-2098
For contact information about worldwide offices, see the MathWorks Web site.
®
Simulink
© COPYRIGHT 2007–20 10 by The MathWorks, Inc.
The software described in this document is furnished under a license agreement. The software may be used
or copied only under the terms of the license agreement. No part of this manual may be photocopied or
reproduced in any form without prior written consent from The MathW orks, Inc.
FEDERAL ACQUISITION: This provision applies to all acquisitions of the Program and Documentation
by, for, or through the federal government of the United States. By accepting delivery of the Program
or Documentation, the government hereby agrees that this software or documentation qualifies as
commercial computer software or commercial computer software documentation as such terms are used
or defined in FAR 12.212, DFARS Part 227.72, and DFARS 252.227-7014. Accordingly, the terms and
conditions of this Agreement and only those rights specified in this Agreement, shall pertain to and govern
theuse,modification,reproduction,release,performance,display,anddisclosureoftheProgramand
Documentation by the federal government (or other entity acquiring for or through the federal government)
and shall supersede any conflicting contractual terms or conditions. If this License fails to meet the
government’s needs or is inconsistent in any respect with federal procurement law, the government agrees
to return the Program and Docu mentation, unused, to The MathWorks, Inc.
Trademarks
MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See
www.mathworks.com/trademarks for a list of additional trademarks. Other product or brand
names may be trademarks or registered trademarks of their respective holders.
Patents
The MathWorks products are protected by one or more U.S. patents. Please see
www.mathworks.com/patents for more information.
Design Verifier™ Release Notes
Summary by Version ............................... 1
Contents
Version 1.6 (R2010a) Simulink
Software
........................................ 4
Version 1.5 (R2009b) Simulink
Software
........................................ 8
Version 1.4 (R2009a) Simulink
Software
........................................ 12
Version 1.3 (R2008b) Simulink
Software
........................................ 16
Version 1.2 (R2008a) Simulink
Software
........................................ 20
Version 1.1 (R2007b) Simulink
Software
........................................ 22
Version 1.0 (R2007a+) Sim ulink
Software
........................................ 23
®
Design Verifier
®
Design Verifier
®
Design Verifier
®
Design Verifier
®
Design Verifier
®
Design Verifier
®
Design Verifier
Compatibility Summary for Simulink
Software
........................................ 25
®
Design Verifier
iii
iv Contents
SummarybyVersion
This table provides quick access to what’s new in each version. For
clarification, see “Using Release Notes” on page 2 .
Simulink®Design Verifier™ Release Notes
Version
(Release)
Latest Versi
V1.6 (R2010a
V1.5 (R2009b)
V1.4 (R2
V1.3 (R2008b)
V1.2.1 (R2008a+)
on
)
009a)
New Features
and Changes
Yes
Details
Yes
Details
Yes
Details
Yes
ls
Detai
No No Bug Reports
Version
Compatibilit
Consideratio
No B ug Reports
Yes
Summary
No B ug Reports
Yes
Summa
ry
Fixed Bugs
y
and Known
ns
Problems
Includes fix
Bug Reports
Includes fixes
Includes fixes
Bug Re
Inclu
Includes fixes
ports
des fixes
Related
Documentation
at Web Site
Printable Release
es
Notes: PDF
Current product
documentation
Printable
Notes: PDF
Current p
document
Printable Release
Notes: PDF
Current product
documentation
Printable Release
Notes: PDF
Current product
documentation
No
Release
roduct
ation
V1.2 (R2008a)
.1.1 (R2007b+)
V1
V1.1 (R2007b)
V1.0 (R2007a+)
Yes
tails
De
No No Bug Reports
Yes
Details
Yes
Details
No Bug
No B ug Reports
No B ug Reports No
Reports
cludes fixes
In
Includes fixes
Includes fixes
No
No
No
1
Simulink®Design Verifier™ Release Notes
Using Release No
Use release note
• New features
• Changes
• Potential imp
Review the re
product (for
bugs, or comp
If you are up
review the c
you upgrad
What Is in t
New Featu
• New func
• Changes
s when upgrading to a new er version to learn about:
act o n your existing files and practices
lease notes for other M athWorks™ products required for this
example, MATLAB
atibility considerations in other products impact you.
grading from a softw are version other than the most recent one,
urrent release notes and all interim versions. For example, when
e from V1.0 to V1.2, review the release notes for V1.1 and V1.2.
he Release Notes
res and Changes
tionality
to existing functionality
tes
®
or Simulink®). Determine if enhancements,
Versio
When a n
versi
impac
Comp
Repo
in in
comp
Fix
The
vi
n Compatibility Considerations
ew feature or change introduces a reported incompatibil ity between
ons, the Compatibility Considerations subsection explains the
t.
atibility issues reported after the product release appear under Bug
rts at The MathWorks™ Web site. Bug fixes can sometimes result
compatibilities, so review the fixed bugs in Bug Reports for any
atibility impact.
ed Bugs and Known Problems
MathWorks offers a user-searchable Bug Reports database so you can
ew Bug Reports. The development team updates this database at release
2
SummarybyVersion
time and as more information becomes available. Bug Reports include
provisions for any known workarounds or file replacem ents. Information is
available for bugs existing in or fixed in Release 14SP2 or later. Information
is not avail able for all bugs in earlier releases.
Access Bug Reports using y our MathWorks Account.
3
Simulink®Design Verifier™ Release Notes
Version 1.6 (R2010a) Simulink Design Verifier Software
This table summarizes what’s new in V1.6 (R2010a):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
None Bug Reports
New features and changes introduced in this version are:
• “Generate Test Cases for Missing Coverage Data” on page 4
• “sldvlogdata Function for Logging Test Cases During Simulation” on page 5
• “Extend Existing Test Cases” on page 5
• “Demo Library and Models to Support Temporal Properties Specification”
on page 5
• “Support for Stateflow Absolute-Time Temporal Logic Operators” on page 6
• “Support for Simulink Blocks” on page 6
Fixed Bugs an d
Known Problems
Related
Documentation at
Web Site
Printable Release
Notes: PDF
Current product
documentation
Generate Test Cases for Missing Coverage Data
The Simulink®DesignVerifier™softwarenowofferstheoptiontoisolate
test generation to objectives that are not satisfied in simulation coverage
results. If you simulate your model, but do not achieve 100% coverage, you
can analyze the model using the Simulink Design Verifier test-generation
capability to find test cases that achieve the missing coverage.
If you select the Ignore objectives satisfied in existing coverage data
parameter in the Configuration Parameters dialog box, you can import the
coverage data file; the analysis eliminates all objectives satisfied in the
coverage results.
4
Version 1.6 (R2010a) Simulink®Design Verifier™ Software
sldvlogdata Function for Logging Test Cases During
Simulation
With the new sldvlogdata function, you can:
• Simulate a Simulink model and in that model, log all the inputs to a Model
block.
• Simulate all or some of the test cases in a harness model created by the
Simulink Design Verifier software and log all the inputs to the test unit.
You can save logged data to a MAT-file and use that file as input to the
Simulink Design Verifier software for extending tests. This allows you to
generate more realistic test cases andextendstheanalysistocompletethe
test suite.
Extend Existing Test Cases
The Simulink Design Verifier software now offers the option to extend
existing test cases with additional time steps to generate complete test suites.
This allows the software to generate test cases for parts of your model that
are hard to analyze.
If you enable the Extend existing test cases parameter in the Configuration
Parameters dialog box, the software imports the logged test cases from a
MAT-file. If you also enable the Ignore objectives satisfied by existing
test cases parameter, the analysis generates results, ignoring the coverage
objectives satisfied by the logged test cases. Otherwise, the analysis efficiently
creates a complete test suite.
Demo Librar y and Models to Support Temporal
Properties Specification
The Simulink Design Verifier software includes a new Temporal Property
Specification demo category that includes:
• A Temporal Operator Blocks demo library that contains the following
blocks and examples:
5
Simulink®Design Verifier™ Release Notes
- Detector — Detects a user-specifie d length of true duration on the input
signal and constructs an output true duration of length based on the
output type.
- Extender — Extends the true duration of the input signal by a fixed
number of time steps or indefinitely.
- Within Implies — Captures the within implication by observing whether
the second input is true for at least one time step within each true
duration of the first input.
- Temporal Property Specification examples — A library model that
includes examples that use the Detector, Extender, and Within Implies
blocks
• Two demo models that contains these blocks:
- Debounce Temporal Properties
- Power Window Controller Temporal Properties
Support for Stateflow Absolute-Time Temporal Logic
Operators
The Simulink Design Verifier software now supports the Stateflo w
absolute-time temporal logic operators. For more information, see “Operators
for Absolute-Time Temporal Logic” in the Stateflow and Stateflow
User’s Guide.
®
®
Coder™
Support for Simulink Blocks
The Simulink De sign Verifier software now fully su pp orts the follow ing blocks:
• Backlash
• Cosine
• Discrete Derivative
• Sine
The Simulink Design Verifier software now provides improved support for
the following blocks:
• Interpolation Using Prelookup
6
Version 1.6 (R2010a) Simulink®Design Verifier™ Software
• Lookup Table (n-D)
For more information, see “Simulink Block Support”.
7
Simulink®Design Verifier™ Release Notes
Version 1.5 (R2009b) Simulink Design Verifier Software
This table summarizes what’s new in V1.5 (R2009b):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
Yes
Summary
• “New Functions for Verification Objectives and Constraints” on page 8
• “Support for Enumerated Signals and Parameters” on page 9
• “New Option to Stop Simulation on Proof Violation” on page 9
• “New sldvmakeharness Function” on page 10
• “New sldvreport Function” on page 10
• “New Support for Simulink Blocks” on page 10
• “Support for New Blocks” on page 10
Fixed Bugs an d
Known Problems
Bug Reports
Related
Documentation at
Web Site
Printable Release
Notes: PDF
Current product
documentation
New Functions for Verification Objectives and
Constraints
Use these four new functions to specify objectives and constraints within
an Embedded MATLAB
corresponding Simulink Design Verifier blocks.
®
script. You can use these functions instead of the
Function
sldv.assume
sldv.condition
sldv.prove
sldv.test
Purpose
Proof assumption Proof Assumption
Test condition
Proof objective Proof Objective
Test objective
Corresponding Block
Test Condition
Test Objective
8
Version 1.5 (R2009b) Simulink®Design Verifier™ Software
These functions:
• Identify mathematical relationships for objectives and constraints in a form
that can be more natural than using block parameters
• Support specifying multiple constraints without complicating the model
• Provide access to the power of the MATLAB software
• Support separation of verification and model design
Compatibility Considerations
The following functions will be removed in a future release:
•
dv.assume
• dv.condition
• dv.prove
• dv.test
To ensure models with those functions will work in future releases, replace
these functions with the corresponding new function added in this release.
For example, replace
dv.assume with sldv.assume.
Support for Enumerated Signals and Parameters
The Simulink D esi gn Verifier software now supports Simulink models wi th
enumerations. Al l the Simulink Design Verifier library blocks support
enumerated parameters, constants, and inputs.
NewOptiontoStopSimulationonProofViolation
The Simulink Design Verifier software allows you to stop a model simulation
if it encounters a property violation. You enable this capability by inserting a
Proof Objective block into a model and setting the Stop simulation when
the property is violated parameter. If the simulation detects a violation of
the property specified in the Proof Objective block, it terminates with an error.
Therefore, you can now verify a counterexample that was detected during a
Simulink Design Verifier analysis.
9
Simulink®Design Verifier™ Release Notes
New sldvmakehar
With the new sldv
• Create a test ha
analysis data.
• Create an empt
New sldvrepo
You can now ge
Verifier ana
lysis data with the new
New Support
The Simuli
and parame
• Direct Lo
• Discrete
• Lookup T
block pa
input an
• Math Fu
transp
nk Design Verifie r software now supports the following blocks
ters:
okup Table (n-D)
Transfer Fcn
able and Lookup Table (2-D) — Unless the Lookup method
rameter specifies
d output signals do not have the same floating-point data type.
nction — All signal types now support the
ose
makeharness
rness model from existing Simulink D es ign Verifier
y test harness m ode l directly from a Simulink model.
rt Function
nerate and customize a report from existing Simulink Design
for Simulink Blocks
function parameter settings
ness Function
function, you can:
sldvreport function.
Interpolation-Extrapolation and the block’s
hermitian and
10
• Rate Li
• Shift
• Tappe
• Tran
• Tran
Sup
The
cks:
blo
• Di
miter — F or signals of all data types
Arithmetic — For all parameters and signals of all data types
dDelay
sfer Fcn Direct Form II
sfer Fcn Direct Form II Time Varying
port for New Blocks
Simulink Design Verifier software supports the following new Simulink
screte PID Controller
• Discrete PID Controller (2 DOF)
• Enumerated Constant
Version 1.5 (R2009b) Simulink®Design Verifier™ Software
11
Simulink®Design Verifier™ Release Notes
Version 1.4 (R2009a) Simulink Design Verifier Software
This table summarizes what’s new in V1.4 (R2009a):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
No Bug Reports
New features and changes introduced in this version are:
• “Automatic Stubbing for Unsupported Operations” on page 12
• “Long Test Case Optimization” on page 13
• “New Support for Blocks” on page 13
• “Analyzing External Functions for Embedded MATLAB Function Blocks”
on page 13
• “Enhanced Block Replacement Capability for Subsystems and Model
Blocks” on page 14
• “New Implies Block” on page 14
• “New Property-Proving Examples and Demos” on page 14
• “sldvisactive Function” on page 15
Fixed Bugs an d
Known Problems
Related
Documentation at
Web Site
Printable Release
Notes: PDF
Current product
documentation
12
Automatic Stubbing for Unsupported Operations
Automatic stubbing allows you to complete a test-generation or
property-proving analys is even if the model contains blocks or functions that
the Simulink Design Verifier software does not support, like S-functions and
Cmathoperations.
By default, this feature is unavailable. To enable automatic stubbing before
running an analysis, on the Configuration Parameters Design Verifier main
pane, select Automatic stubbing of unsupported blocks and functions.
Version 1.4 (R2009a) Simulink®Design Verifier™ Software
In addition, if the compatibility check finds unsupported blocks that automatic
stubbing can handle, you can enable automatic stubbing at that time.
Long Test Case Optimization
Long test cases is a new option for the Test suite optim ization
parameter. The
Verifier software to create fewer but longer test cases that each satisfy
multiple test objectives. With this option, you can customize the analysis
results, run a more efficient analysis, and create easier-to-review resu lts, in
both Signal Builder and in the HTML report that the software generates.
Long test cases option instructs the Simulink Design
New Support for Blocks
The Simulink Desi gn Verifier software now supports models containing the
following blocks:
• Combinatorial Logic
• Decrement Time To Zero
• Discrete Filter
• Fixed-Point State-Space
• Integer Delay
• Model blocks that reference other models
• Prelookup
• Relay
AnalyzingExternalFunctionsforEmbeddedMATLAB
Function Blocks
If your model contains an Embedded MATLAB Function block that calls any
external functions, the Simulink Desig n Verifier software can now accumulate
coverage results for those functions.
13
Simulink®Design Verifier™ Release Notes
Enhanced Block Replacement Capability for
Subsystems and Model Blocks
You can write your own replace m ent rules to replace subsystem or Model
blocks that reference a nother model w it h the Simulink Design Verifier block
replacement capability. The software replaces a subsystem or Model block
with a different subsystem or with a built-in block a s defined in the block
replacement rules.
New Implies Block
The new Implies block simplifies property specification. You can now specify
conditions that produce a given response. For example, you can quickly
create expressions indicating that pressing the break pedal implies the cruise
control must be inactive.
You can use the Implies block in any model, not just when running the
Simulink Design Verifier software.
14
New Property-Proving Exam ples and Demos
The Simulink Design Verifier block library includes four new example models
that demonstrate how to define complex properties for property-proving
analysis.
In addition, the following demo models are shipping with R2009a:
•
sldvdemo_sbr_design.mdl — Finding property violations
sldvdemo_sbr_verification.mdl — Proving that properties are valid
•
sldvdemo_thrustrvs_verification.mdl — Analyzing model and
•
properties to prove correctness or to identify counterexamples
•
sldvdemo_cruise_control_fxp_verification.mdl — Proving properties
for fixed-point arithmetic with block replacements
•
sldvdemo_cruise_control_verification.mdl — Supporting model
reference and verification subsystems
Version 1.4 (R2009a) Simulink®Design Verifier™ Software
sldvisactive Fu
e
The sldvisactiv
software is acti
the masked init
callbacks to co
analysis.
For example, t
invokes the
you start ana
s
function checks whether the Simulink Design Verifier
vely translating the model. This function is called from
ialization of masked subsystems and other model or block
nfigure the model, as needed, for Simulink Design Verifier
he mask initialization of the Environment Controller block
ldvisactive
lyzing a model that contains the block.
nction
function to output the signal at its Sim port when
15
Simulink®Design Verifier™ Release Notes
Version 1.3 (R2008b) Simulink Design Verifier Software
This table summarizes what’s new in V1.3 (R2008b):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
Yes
Summary
New features and changes introduced in this version are:
• “Simulink Bus Signals and Bus Objects Support ” on page 16
• “Fixed-Point Data Support” on page 17
• “Generating Test Harness Model with Model Reference” on page 17
• “Generating SystemTest TEST-File” on page 17
• “Improved Search Algorithms” on page 17
• “New Data File Format” on page 18
• “New HTML Report” on page 18
• “Blocks with No Input Ports Limitation” on page 19
Fixed Bugs an d
Known Problems
Bug Reports
Related
Documentation at
Web Site
Printable Release
Notes: PDF
Current product
documentation
Simulink Bus Signals and Bus Objects Support
Simulink Design Verifier now supports Simulink buses and bus objects:
16
• The root Inport and Outport blocks accept bus signals.
• Nonvirtual buses are propagated through the model elements.
• The test harness model reconstructs the needed bus signals from the
underlying bus elements.
Version 1.3 (R2008b) Simulink®Design Verifier™ Software
Fixed-Point Dat
Simulink Design
inputs. These bl
• Test Condition
• Test Objectiv
• Assumption
• Proof Object
The
Slvd.Po
Generating
To use this
the Design
box. Simul
original
ink Design Verifier software then uses model reference to run the
model from the test harness.
Generat
To use th
the Desi
box. Th
aTESTand con
is option, select Save test harness as SystemTest TEST-File in
gn Verifier > Results pane of the Configuration Parameters dialog
e software creates a TEST-file instead of a test harness model. Using
fileallowsyoutorunthetestcasesin the SystemTest™ environment
figure the model coverage settings using the SystemTest software.
Verifier blocks now support fixed-point parameters and
ocks include:
e
ive
int
and Sldv.Interval constructors now accept fixed-point data.
Test Harness Model with Model Reference
option, select Reference input model in generated harness in
Verifier > Results pane of the Configuration Parameters dialog
ing SystemTest TEST-File
a Support
Impro
This r
impr
• Test
• Pro
ved Search Algorithms
elease includes search algorithms for the following two modes that
ove the performance and the quality of the results:
case generation — The combined objectives options minimizes the
er of test cases by generating cases that address more than one test
numb
ective.
obj
perty proving — Proving that model properties are valid.
17
Simulink®Design Verifier™ Release Notes
New Data File For
When the Simulin
adatafile. Nowt
information ab
Simulink Desig
documentatio
k Design Verifier software completes an analysis, it creates
he data file supports bus input ports and includes more
out the analyzed model. For more information, see “Examining
n Verifier Data Files” in the Simulink Design Verifier
n.
mat
Compatibility Considerations
To convert an
Sldv.Dat
the
syntax:
new_sldvData = Sldv.DataUtils.convertToCurrentFormat(model, old_sldvData)
The arguments used for this conversion comprise:
•
model — The name of the model that was analyzed
old_sldvData — The name of an sldvData structure created using the old
•
(pre-R2008b) format
To convert an
Sldv.DataUtils.convertToOldFormat utility with the following syntax:
sldvData structure from the old format to the new format, use
aUtils.convertToCurrentFormat
sldvData structure in the new format to the old format, use the
utility with the following
18
old_sldvData = Sldv.DataUtils.convertToOldFormat(model, new_sldvData)
The arguments used for this conversion comprise:
•
model — The name of the model that was analyzed
new_sldvData — The name of an sldvData structure created using the
•
format that is new with R2008b
New HTML Report
The HTML report that Simulink D esign Verifier so ftware generates has been
enhanced. Now, when you select Generate report of the results in the
Design Verifier > Report pane of the Configuration Parameters dialog box,
the report generated has several improvements:
• The report generate s faster and is easier to understand.
Version 1.3 (R2008b) Simulink®Design Verifier™ Software
• The report can display expected outputs.
• The software generates a report that reflect the analysis settings (for
example, test case generation vs. property proving).
Blocks with No Input Ports Limitation
If a Simulink model has any blocks with no input ports, Simulink Design
Verifier software cannot generate the test harness.
19
Simulink®Design Verifier™ Release Notes
Version 1.2 (R2008a) Simulink Design Verifier Software
This table summarizes what’s new in V1.2 (R2008a):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
No Bug Reports
New features and changes introduced in this version are
• “Embedded MATLAB Subset Support” on page 20
• “Enhanced Support for Stateflow Truth Tables” on page 20
• “New Simulink
• “New Test Suite Optimization Setting” on page 21
®
Design Verifier Data File Options” on page 20
Fixed Bugs an d
Known Problems
Related
Documentation at
Web Site
Printable Release
Notes: PDF
Current product
documentation
Embedded MATLAB Subset Support
This release provides support for the Embedded MATLAB Function block in
the Simulink software and Embedded MATLAB functions in the Stateflow
software. For more information, see “Support Limitations for the Embedded
MATLAB Subset” in the Simulink Design Verifier User’s Guide.
20
Enhanced Support for Stateflow Truth Tables
Previous releases support only the Stateflow Classic truth tables. However,
this release introduces support for Embedded MATLAB truth tables in the
Stateflow software, which includes support for the Truth Table block. See
“Truth Table Functions” in the Stateflow documentation for more information.
New Simulink Design Verifier Data File Options
This releas e introduces new options on the Design Verifier > Results pane
of the Configuration Parameters dialog box:
Version 1.2 (R2008a) Simulink®Design Verifier™ Software
• Include expected output values — Simulates the model using the test
case signals and includes the output values in the Simulink Design Verifier
data file. See “Include expected outp u t values” for more information.
• Randomize data that does not affect outcome — Assigns random
values instead of zeros to input signals that have no impact on test or proof
objectives. See “Randomize data that does not affect outcome” for more
information.
New Test Suite Optimization Setting
In this release, the Test suite optimization parameter that appears on the
Design Verifier > Test Generation pane of the Configuration Parameters
dialog box includes a new setting:
is tailored to large, complex models that contain nonlinearities and many test
objectives. See “Test suite optimization” for more information.
Large model. This test generation strategy
21
Simulink®Design Verifier™ Release Notes
Version 1.1 (R2007b) Simulink Design Verifier Software
This table summarizes what’s new in V1.1 (R2007b):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
No Bug Reports No
Fixed Bugs an d
Known Problems
Related
Documentation at
Web Site
Fixed-Point Data Type Support
This release provides support for fixed-point data types. For more information,
see “Fixed-Point Support Limitations” in the Simulink Design Verifier User’s
Guide.
22
Version 1.0 (R2007a+) Simulink®Design Verifier™ Software
Version 1.0 (R2007a+) Simulink Design Verifier Software
This table summarizes what’s new in V1.0 (R2007a+):
New Features and
Changes
Yes
Details below
Version
Compatibility
Considerations
No Bug Reports No
Version 1.0 of the Simulink Design Verifier software was released in a
Web-downloadable form after R2007a.
Fixed Bugs an d
Known Problems
Related
Documentation at
Web Site
Introducing the Simulink Design Verifier Software
The Simulink Design Verifier softwa reextendstheSimulinkandStateflow
products with formal methods that help you confirm your models and
charts behave correctly. The Simulink Design Verifier software performs a
mathematically rigorous a nalysis of your model to identify all of its possible
execution pathways. Subsequently, the software can
• Generate Tests
The Simulink Design Verifier software can generate tests that satisfy
your model’s coverage objectives, including decision coverage, condition
coverage, and modified condition/decision coverage (MC/DC). You can even
customize the tests that it generates by using Simulink Design Verifier
blocks that allow you to specify your own objectives and to constrain signal
values. After the software completes its analysis, it produces a test harness
model with a Signal Builder b l ock that contains test signals. Simply
simulate the test harness model to confirm that the test signals achieve
your model’s objectives.
• Prove Properties
The Simulink Design Verifier software can prove tha t signals in your
model attain particular values or ranges. Use Simulink Design Verifier
blocks to specify values and ranges that you desire signals to attain, or
to constrain the values of other signals. If the software disproves any of
thevaluesorrangesgiventheconstraints you specify, it produces a test
23
Simulink®Design Verifier™ Release Notes
harness model with a Signal Builder block that contains signals comprising
counterexamples. Simply simulate the test harness model to confirm that
the counterexamples falsify your model’s properties.
The Simulink D esign Verifier software documents its an alysis results in an
HTML report. Also, it produces a data file containing the analysis results,
which you can postprocess for your own analyses and reports.
In short, the Simulink Design Verifier software gives you confidence in the
behavior of your Simulink models and Stateflow charts.
24
Compatibility Summary for Simulink®Design Verifier™ Software
Compatibility Summary for Simulink Design Verifier
Software
This table summarizes new features and changes that might cause
incompatibilities when you upgrade from an earlier version, or wh en you
use files on multiple versions. Details are provided in the description of the
new feature or change.
Version (Release) New Features and Changes with
Version Compatib ility Impact
Latest Version
V1.6 (R2010a)
V1.5 (R2009b) See the Compatibility
V1.4 (R2009a)
V1.3 (R2008b) See the Compatibility
V1.2 (R2008a)
V1.1 (R2007b)
V1.0 (R2007a+)
None
Considerations subheading
for:
• “New Functions for Verification
Objectives and Constraints” on
page 8
None
Considerations subheading
for:
• “New Data File Format” on page
18
None
None
None
25
Loading...