Software hazard generation with model checking

Phongphun Kijsanayothin, Rattikorn Hewett, Jingsong Wang, Meinhard Peters

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


The problem of finding hazards associated with software becomes more necessary if not critical as modern systems increasingly rely on software to provide their main functionalities. While verification and validation can help determine whether software behaves correctly according to its specifications and user needs, they cannot guarantee that software will not lead to system hazards particularly when it interacts with the environments unanticipated by the software designer. Most existing hazard identification techniques require laborious and time-consuming analysis that often either ignores detailed software properties or does not specifically address software-related hazards. This paper presents an approach that facilitates a semi-automated hazard identification of computer-based systems by a novel application of model checking, a technique traditionally used for automated software verification. Our work is in a preliminary stage. The paper describes the approach and illustrates its use to identify hazardous conditions that could lead to violation of system safety.

Original languageEnglish
Title of host publication2006 IEEE Region 5 Conference
PublisherIEEE Computer Society
Number of pages6
ISBN (Print)1424403596, 9781424403592
StatePublished - Jan 1 2006
Event2006 IEEE Region 5 Conference - San Antonio, TX, United States
Duration: Apr 7 2006Apr 8 2006

Publication series

Name2006 IEEE Region 5 Conference


Conference2006 IEEE Region 5 Conference
Country/TerritoryUnited States
CitySan Antonio, TX


Dive into the research topics of 'Software hazard generation with model checking'. Together they form a unique fingerprint.

Cite this