Simulink/T-VEC Examples

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

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.

Contents

Key Guidelines

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

Signal ranges information defines the low bound and high bound values of input and output signals. This information is critical because test vector inputs are selected based on the range of the input signals. In addition, T-VEC analyzes the model using domain analysis starting from the signal range. The default input ranges are based on type definition. The min (low bound) and max (high bound) values often do not make sense. This especially true for floating-point numbers that have the following ranges:

  • 32 bit float range: -3.4E+38 to 3.4E+38
  • 64 bit float range: -1.7E+308 to 1.7E+308

Selecting values in very large ranges degrades precision, for examples:

Y < X + 100 when X is 1.7E+308 is not meaningful
Value of 100 is lost in the noise of 1.7E+308

Default ranges for floating point types set to reduce problems

  • single (32 bit float) range: -1.0e4..1.0e4
  • double (64 bit float) range: -1.0e12..1.0e12

Other types have default ranges

  • int8: -128..127 int16: -32768..32767
  • unint8: 0..255 uint16: 0..65535
  • int32: -2147483648.. 2147483647
  • uint32: 0..4294967295

The default type ranges can be modified or specific signal ranges can be defined by the users. These operations can be performed using the Signal Range Editor GUI or they can be done to the underlying file (XML) using an editor.

To create a default, run the SL2TVEC translation once, then use the Signal Range Editor to appropriately set the signal ranges.

Test Sequences

Assertions

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