Fault-injection through model checking via naive assumptions about state machine synchrony semantics

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.

Name thesis:degree_name

MS

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Lane Department of Computer Science and Electrical Engineering

Year dc:date.available

1998

Author dc:creator

• Joseph, Sabina

Contributors dc:contributor

• Jack Callahan.

• Computer science
• Electrical engineering

Identifier

https://researchrepository.wvu.edu/etd/913

OAI identifier oai:identifier

oai:researchrepository.wvu.edu:etd-1916