Difference between revisions of "Modeling"
|Line 13:||Line 13:|
The [[T-VEC_Vector_Generation_System#Test_Vector_Generation|test vector generator]] performs [[Formal_Methods_and_Theorem_Provers#Model Checking Supports Testing|model checking]] on a DCP at each level in the hierarchy, and
The [[T-VEC_Vector_Generation_System#Test_Vector_Generation|test vector generator]] performs [[Formal_Methods_and_Theorem_Provers#Model Checking Supports Testing|model checking]] on a DCP at each level in the hierarchy , and that
are error freeproduces as a byproduct a test vector. The tools integrate with a [[T-VEC_Vector_Generation_System#Test_Driver_Generation|test driver generator]] to produce test drivers that automate test execution for most any language and test environment with automated test results analysis.
Revision as of 13:36, 15 February 2007
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 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.