Difference between revisions of "Modeling"

From T-VEC Wiki
Jump to: navigation, search
 
 
Line 1: Line 1:
 
There are many types of models and modeling notations. The support T-VEC tools provide include functional [[T-VEC_Tablular_Modeler#Requirement Modeling|Requirement Models]], [[Simulink Tester for T-VEC#Design Model|Design Models]], and [[Simulink Tester for T-VEC#Hybrid Model|Hybrid Models]].
 
There are many types of models and modeling notations. The support T-VEC tools provide include functional [[T-VEC_Tablular_Modeler#Requirement Modeling|Requirement Models]], [[Simulink Tester for T-VEC#Design Model|Design Models]], and [[Simulink Tester for T-VEC#Hybrid Model|Hybrid Models]].
  
==Model Representation==
+
==Model Types==
  
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.
+
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).  
  
[[Image:Model_Spectrum.jpg|Model Spectrum]]
+
[[Image:Model_Spectrum.jpg|center|Model Spectrum]]
  
==Modeling Transforms==
+
===High 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 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|Test Sequence Vectors]].
+
The translators for both TTM and SL2TVEC perform model 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. The subsystems are derived from the modeling constructs of TTM (e.g., condition tables) and Simulink subsystems.  
  
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 T-VEC standard language 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. Subsystems can have a hierarchical relationships, where higher-level subsystems can reference lower-level subsystems (some times referred to as utilities). Subsystem references have a functional syntax (e.g., output = function(input1, ..., inputN)).
 +
 
 +
===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 retain their grouping within the subsystems of the higher-level representation. 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|Test Sequence Vectors]].
  
 
==Tool Flow==
 
==Tool Flow==
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 DCPs that are error free produces 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.
+
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 during test vector generation, and T-VEC VGS creates reports identifying the [[VGS_Advanced_Topics#Failure_Analysis|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 [[VGS_Advanced_Topics#Failure_Analysis|model defect]]. Coverage reports link to detailed error reports that link a DCP problem through the subsystem standard form to the TTM or Simulink model.
 +
 
 +
If the DCPs are error free, VGS produces 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.

Latest revision as of 12:09, 26 February 2007