Recently model checkers have been applied to software areas such as analyzing protocols and algorithms, measuring test adequacy, and generating abstract tests from formal models. When using model checkers to generate tests, the generated tests are execution traces of the models. Thus the type, occurrence, and order of variables, calls, and events in the execution traces are intimately tied to the choice of modeling representation. We briefly review how to use a model checker to generate tests from a high-level representation, such as MATLAB(R), UML, or SCR. Since the model checker uses a particular general model, the analyst has choices about how a piece of software may be modeled. We list some choices and discuss their advantages and disadvantages. We also describe a program to marshal model variables from resultant model checker traces and translate them into function calls, program variables, and other software artifacts.
Modeling and marshaling: making tests from model checker counterexamples
19th DASC. 19th Digital Avionics Systems Conference. Proceedings (Cat. No.00CH37126) ; 1 ; 1B3/1-1B3/6 vol.1
2000-01-01
463062 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Modeling and Marshaling: Making Tests from Model Checker Counterexamples
British Library Conference Proceedings | 2000
|Commutation circuit, flexible marshaling unit and flexible marshaling method
Europäisches Patentamt | 2022
|Europäisches Patentamt | 2024
|Vehicle marshaling method and device and terminal equipment
Europäisches Patentamt | 2021
|VEHICLE MARSHALING METHOD, APPARATUS AND SYSTEM, VEHICLE, AND STORAGE MEDIUM
Europäisches Patentamt | 2022
|