Simulink/T-VEC Examples

From T-VEC Wiki
Revision as of 16:28, 14 February 2007 by Admin (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

The most successful users of T-VEC Tester for Simulink (SL2TVEC) follow a few key guidelines:

  1. They development the models with verification in mind - they are aware of those modeling constructs and patterns that result in safe systems
  2. They perform modeling and the verification activities supported by SL2TVEC iteratively
  3. Understand the tool is performing model checking, and that tests are a byproduct of this process
  4. Understand that the Simmulink/Stateflow tool is continously evolving, and the SL2TVEC integration process may take time to catchup to the changes in every new Simulink release, which further emphasizes point #1.


Key Guideline

This section first discusses some key elements that must be used to support and configure the model translation that results in a T-VEC project for model analysis and test generation.

Signal Ranges

Test Sequences


Assertions are general purpose mechanisms that can be used to specify additional constraint that are external to the model. Such constraints can be used for:

  • Defining implicit design constraint such as natural laws
  • Modeling safety properties
  • Defining additional tests

Example Links