TY - GEN
T1 - On the distribution of property violations in formal models
T2 - 30th Annual International Computer Software and Applications Conference, COMPSAC 2006
AU - Gao, Jimin
AU - Heimdahl, Mats
AU - Owen, David
AU - Menzies, Tim
N1 - Copyright:
Copyright 2011 Elsevier B.V., All rights reserved.
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=34247486197&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34247486197&partnerID=8YFLogxK
U2 - 10.1109/COMPSAC.2006.64
DO - 10.1109/COMPSAC.2006.64
M3 - Conference contribution
AN - SCOPUS:34247486197
SN - 0769526551
SN - 9780769526553
T3 - Proceedings - International Computer Software and Applications Conference
SP - 150
EP - 157
BT - Proceedings - 30th Annual International Computer Software and Applications Conference, COMPSAC 2006
Y2 - 17 September 2006 through 21 September 2006
ER -