Fault-injection through model checking via naive assumptions about state machine synchrony semantics
Semester
Fall
Date of Graduation
1998
Document Type
Thesis
Degree Type
MS
College
Statler College of Engineering and Mineral Resources
Department
Lane Department of Computer Science and Electrical Engineering
Committee Chair
Jack Callahan.
Abstract
Software behavior can be defined as the action or reaction of software to external and/or internal conditions. Software behavior is an important characteristic in determining software quality. Fault-injection is a method to assess software quality through its' behavior. Our research involves a fault-injection process combined with model checking. We introduce a concept of "naive assumptions" which exploits the assumptions of execution order, synchrony and fairness. "Naive assumptions" are applied to inject faults into our models. We use linear temporal logic to examine the model for anomalous behaviors. This method shows us the benefits of using fault-injection and model checking and the advantage of the counter-examples generated by model checkers. We illustrate this technique on a fuel injection Sensor Failure Detection system and discuss the anomalies in detail.
Recommended Citation
Joseph, Sabina, "Fault-injection through model checking via naive assumptions about state machine synchrony semantics" (1998). Graduate Theses, Dissertations, and Problem Reports. 913.
https://researchrepository.wvu.edu/etd/913