On the distribution of property violations in formal models: An initial study

Jimin Gao, Mats Heimdahl, David Owen, Tim Menzies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Model-checking techniques are successfully used in the verification of both hardware and software systems of industrial relevance. Unfortunately, the capability of current techniques is still limited and the effort required for verification can be prohibitive (if verification is possible at all). As a complement, fast, but incomplete, search tools may provide practical benefits not attainable with full verification tools, for example, reduced need for manual abstraction and fast detection of property violations during model development. In this report we investigate the performance of a simple random search technique. We conducted an experiment on a production-sized formal model of the mode-logic of a flight guidance system. Our results indicate that random search quickly finds the vast majority of property violations in our case-example. In addition, the times to detect various property violations follow an acutely right-skewed distribution and are highly biased toward the easy side. We hypothesize that the observations reported here are related to the phase transition phenomenon seen in Boolean satisfiability and other NP-complete problems. If so, these observations could be revealing some of the fundamental aspects of software (model) faults and have implications on how software engineering activities, such as analysis, testing, and reliability modeling, should be performed.

Original languageEnglish (US)
Title of host publicationProceedings - 30th Annual International Computer Software and Applications Conference, COMPSAC 2006
Pages150-157
Number of pages8
DOIs
StatePublished - 2006
Event30th Annual International Computer Software and Applications Conference, COMPSAC 2006 - Chicago, IL, United States
Duration: Sep 17 2006Sep 21 2006

Publication series

NameProceedings - International Computer Software and Applications Conference
Volume1
ISSN (Print)0730-3157

Other

Other30th Annual International Computer Software and Applications Conference, COMPSAC 2006
CountryUnited States
CityChicago, IL
Period9/17/069/21/06

Fingerprint Dive into the research topics of 'On the distribution of property violations in formal models: An initial study'. Together they form a unique fingerprint.

Cite this