On the Distribution of Property Violations in Formal Models: An Initial Study

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 eas...

• Type: Conference
• Year: 2006
• Where: COMPSAC
• Authors: Jimin Gao, Mats Per Erik Heimdahl, David Owen, Tim Menzies
• Keywords: COMPSAC 2006, Property Violations, Random Search, Software Engineering, Various Property Violations