Paper Info
Title
Using Modechart Modules for Testing Formal Specifications
Abstract
Automated model-checking of formal specifications for real-time systems has remained an elusive goal due to the {\em state-space} explosion problem. This paper describes an approach to testing formal specifications using automatically generated testing modules. This technique preserves many of the advantages of using formal specifications while mitigating the state-space explosion problem by focusing state-space exploration to a subset determined by the test. Because the testing modules are defined in the same formalism as the specification, the semantics of the test are precisely defined. Moreover, existing model-checking tools can be leveraged to perform the testing. Finally, this approach reduces evaluation of a potential complex assertion to a simple reachability condition in the tested specification's state space.
Year
DOI
Venue
1999
10.1109/HASE.1999.809471
HASE
Keywords
Field
DocType
explosion problem,testing formal specifications,automated model-checking,em state-space,formal specification,modechart modules,state-space exploration,potential complex assertion,state-space explosion problem,elusive goal,model-checking tool,testing module,subroutines,model checking,system testing,computer science,state space,conformance testing,computer aided software engineering,automatic control,real time systems,formal specifications
Programming language,Computer science,System testing,Functional testing,Real-time computing,Reachability,Formal specification,Conformance testing,Formal methods,Computer-aided software engineering,State space
Conference
ISBN
Citations 
PageRank 
0-7695-0418-3
1
0.36
References 
Authors
7
1
Name
Order
Citations
PageRank
Monica Brockmeyer19111.95