%0 Journal Article
%T Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications
%A Salamah Salamah
%A Ann Q. Gates
%A Steve Roach
%A Matthew Engskow
%J Advances in Software Engineering
%D 2011
%I Hindawi Publishing Corporation
%R 10.1155/2011/869182
%X The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the B¨¹chi automaton generated for the formula. Minimizing the size of the B¨¹chi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker. 1. Introduction The process of model checking a system consists of developing a model of the system to be verified and writing specifications in a temporal logic such as Linear Temporal Logic (LTL) [1] or Computational Tree Logic (CTL) [2]. In automata-based model checking, both the model and the complement of the temporal specification are represented by a special type of state machine called a B¨¹chi Automaton (BA) [3]. To check the consistency of with , the model checker calculates the intersection of and where is the complement of . If the intersection is empty, then is consistent with . In other words, if and each represent a set of specifications and if , then the system satisfies the specification; otherwise, the system is inconsistent with the specification and a counter-example is returned. The process of writing formal specifications is not easy because of the required mathematical sophistication and depth of knowledge in the specification language. For this reason, tools that simplify the creation of formal specifications in logics such as LTL are of interest to the model checking community and others. In the case of automata-based model checkers such as Spin [4], it is important that these tools generate efficient formulas, since the model checker complements the formulas, translates the result into a BA, and intersects the BA with the automaton of the system. The size of the automaton that results from the intersection of two automata has as its upper bound the product of the number of states in each of the two. One way to avoid the classical problem of state space explosion is to minimize the number of states generated by the negation of the specification. This will reduce the number of states generated by the automaton of the intersection, and as a result, it will reduce the time required to model check a software system. The Property Specification (Prospec) [5¨C7] builds on the
%U http://www.hindawi.com/journals/ase/2011/869182/