|
Published Articles >> Table of Contents >> Abstract
Seventh IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'01)
p. 0212
Using a Model Checker to Test Safety Properties
Paul Ammann, George Mason University
Wei Ding, George Mason University
Daling Xu, George Mason University
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.2001.930180
Send link to a friend
| Abstract |
|
Abstract: In addition to providing a sound basis for analysis, formal methods can support other development activities; in our case the target is specification-based testing at the system level. We use the formal method of model checking to either generate new test sets or analyze existing test sets with respect to safety properties expressed in a temporal logic. We consider two types of tests: failing tests, in which a system must reject (fail) a specific dangerous action, and passing tests, in which a system must accept (pass) a safe action in a context that also includes a plausible dangerous action. We formalize our notion of dangerous actions with a mutation model for model checking specifications, and we develop coverage criteria to assess test sets. The coverage criteria are based on the logic operators from the Computation Tree Logic (CTL) and encompass the idea of scenarios where a dangerous action is either inevitable (A) or possible (E) as of the next state (X) or at some point in the future (F). We demonstrate the feasibility of our approach with an example.
|
 Additional Information
|
Index Terms- Model checking, Mutation analysis, Software testing, Safety.
Citation:
Paul Ammann, Wei Ding, Daling Xu,
"Using a Model Checker to Test Safety Properties,"
iceccs,
p. 0212,
Seventh IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'01),
2001
|
|
