As shown in the figure, TTM provides constructs and a language to define requirement models. Simulink/Stateflow provide constructs and a language to define design models. TTM and the assertion mechanism supported by the Simulink Tester for T-VEC (SL2TVEC) provide a language and approach for defining properties (e.g., safety properties, security properties). The translators for both TTM and SL2TVEC perform modeling transformations based on translation options that result in a high-level representation called a T-VEC project that is composed of T-VEC subsystems. The subsystem language is called the T-VEC standard form. It is a textual (ASCII) language. Simplistically stated, each subsystem has one or more Functional Relationships (FRs) each associated with one or more Disjunctions (constraints). During the Build process, the T-VEC compiler converts this language into a low-level representation.
At the lowest-level of representation there are Domain Convergence Paths (DCPs) that are conjunctions of predicates, each associated with a functional relationship (FR) that is also treated as a predicate. Sets of DCPs are grouped into subsystems. The grouping is derived from the modeling constructs of TTM (e.g., condition tables) and Simulink subsystems. A DCP can represent a simple precondition/postcondition relationship, but the DCP can represent a complex relationship over time. This supports the ability to generate Test Sequence Vectors.
The underlying specification language of T-VEC supports traditional logical and relational operators, but provides also support for mathematical operators (e.g., trigonometric, intrinsic, integrators, quantization, matrix) to specify functional behavior supporting various applications domains.
The test vector generator performs model checking on a DCP at each level in the hierarchy during test vector generation, and T-VEC VGS creates reports identifying the defects. A simple example of a model defect is a logical contradiction, where a constraint such as (x > 0) & (x < 0) is in the DCP specification. Model checking hierarchically composed subsystems involves checking the satisfiability of constraint or function references between higher-level (i.e., grandparent) and lower-level (i.e., child) subsystems. For example, as conceptually shown the figure, if there is a constraint, x > 0 in a DCP thread from the grandparent subsystem to a child subsystem, there must be at least one DCP through the parent and child that permits x > 0. If such a constraint in the grandparent cannot be satisfied, then the input space for that DCP of the grandparent is empty (i.e., null), and no test inputs can be selected; this is a model defect.
If the DCPs are error free, VGS produces as a byproduct a test vector. The tools integrate with a test driver generator to produce test drivers that automate test execution for most any language and test environment with automated test results analysis.