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.
At the lowest-level of representation there are Domain Convergence Paths (DCPs) that are conjunctions of predicates, each associated with a functional relationship that is also treated as a predicate. Sets of DCPs are grouped in 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 support 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) that extend standard arithmetic operators to specify functional behavior supporting various applications domains.
The test vector generator performs model checking on a DCP at each level in the hierarchy, and DCPs that are error free 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.