{"id":{"repo_id":"wvu","oai_identifier":"oai:researchrepository.wvu.edu:etd-1916"},"canonical_url":"https://search.dev.ndltd.org/etd/wvu/oai:researchrepository.wvu.edu:etd-1916","repository":{"repo_id":"wvu","name":"West Virginia University","base_url":"https://researchrepository.wvu.edu/do/oai/"},"display":{"title":"Fault-injection through model checking via naive assumptions about state machine synchrony semantics","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Joseph, Sabina"],"institution":null,"degree_name":"MS","degree_level":"Thesis","degree_discipline":"Lane Department of Computer Science and Electrical Engineering","degree_department":null,"school":null,"contributors":["Jack Callahan."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":1998,"date_issued":"1998-12-01T08:00:00Z","date_published":"1998-12-01T08:00:00Z","updated_at":"2026-07-24T06:15:01Z","subjects":["Computer science","Electrical engineering"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://researchrepository.wvu.edu/etd/913"],"render_values":[{"text":"https://researchrepository.wvu.edu/etd/913","href":"https://researchrepository.wvu.edu/etd/913","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.33915/etd.913","outbound_label":"DOI","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Jack Callahan."]},{"key":"dc:creator","label":"Author","values":["Joseph, Sabina"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.available","label":"Dc Date Available","values":["2019-01-17T08:00:00Z"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Lane Department of Computer Science and Electrical Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer science","Electrical engineering"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://doi.org/10.33915/etd.913","https://researchrepository.wvu.edu/etd/913"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Fault-injection through model checking via naive assumptions about state machine synchrony semantics"]}]}],"canonical_facts":{"dc:contributor":["Jack Callahan."],"dc:creator":["Joseph, Sabina"],"dc:date.available":["2019-01-17T08:00:00Z"],"dc:description.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."],"dc:identifier":["https://doi.org/10.33915/etd.913","https://researchrepository.wvu.edu/etd/913"],"dc:subject":["Computer science","Electrical engineering"],"dc:title":["Fault-injection through model checking via naive assumptions about state machine synchrony semantics"],"thesis:degree_discipline":["Lane Department of Computer Science and Electrical Engineering"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T06:15:01Z"}