Date of Graduation
Statler College of Engineering and Mineral Resources
Lane Department of Computer Science and Electrical Engineering
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.
Joseph, Sabina, "Fault-injection through model checking via naive assumptions about state machine synchrony semantics" (1998). Graduate Theses, Dissertations, and Problem Reports. 913.