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–7] builds on the
References
[1]
Z. Manna and A. Pnueli, “An anchored version of the temporal framework,” in Proceedings of the REX Workshop, vol. 354 of LNCS, Springer, Mook, The Netherlands, May 1989.
[2]
F. Laroussinie and PH. Schnoebelen, “Specification in CTL + past for verification in CTL,” Information and Computation, vol. 156, no. 1-2, pp. 236–263, 2000.
[3]
E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, MIT Publishers, Cambridge, Mass, USA, 1999.
[4]
G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, Boston, Mass, USA, 2004.
[5]
O. Mondragon, A. Q. Gates, and S. Roach, “Prospec: support for elicitation and formal specification of software properties,” in Proceedings of the Runtime Verification Workshop, O. Sokolsky and M. Viswanathan, Eds., vol. 89, ENTCS, Boulder, Colo, USA, July 2003.
[6]
O. A. Mondragon and A. Q. Gates, “Supporting elicitation and specification of software properties through patterns and composite propositions,” International Journal of Software Engineering and Knowledge Engineering, vol. 14, no. 1, pp. 21–41, 2004.
[7]
O. Mondragon, Elucidation and specification of software properties through patterns and composite propositions to support formal verification techniques, Ph.D. thesis, The University of Texas, El Paso, Tex, USA, 2004.
[8]
M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Property specification patterns for finite-state verification,” in Proceedings of the 2nd Workshop on Formal Methods in Software Practice, pp. 7–15, Clearwater Beach, Fla, USA, March 1998.
[9]
M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Patterns in property specifications for finite state verification,” in Proceedings of the 21st International Conference on Software Engineering, pp. 411–420, Los Angeles, Calif, USA, May 1999.
[10]
D. Oddoux and P. Gastin, “Fast LTL to Büchi automata translation,” in Proceedings of the 13th International Conference on Computer Aided Verification (CAV '01), Paris, France, July 2001.
[11]
K. Etessami and G. Holzmann, “Optimizing büchi automata,” in Proceedings of the 11th International Conference on Concurrency Theory, August 2000.
[12]
C. Fritz, “Constructing büchi automata from linear temporal logicusing simulation relations for alternating büchi automata,” in Proceedings of the Eighth Conference on Implementation and Application of Automata, Santa Barbara, Calif, USA, July 2003.
[13]
Z. Manna and A. Pnueli, “Completing the temporal picture,” Theoretical Computer Science, vol. 83, no. 1, pp. 97–130, 1991.
[14]
A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, “NUSMV: a new symbolic model verifier,” in Proceedings of the International Conference on Computer Aided Verification (CAV '99), Trento, Italy, July 1999.
[15]
K. Havelund and T. Pressburger, “Model checking Java programs using Java PathFinder,” In- ternational Journal on Software Tools for Technology Transfer, vol. 2, no. 4, pp. 366–381, 2000.
[16]
V. Stolz and E. Bodden, “Temporal assertions using aspectJ,” in Proceedings of the Fifth Workshop on Runtime Verification, The University of Edinburgh, Scotland, UK, July 2005.
[17]
E. Gamma and R. Helm, Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley Professional, Boston, Mass, USA, 1995.
[18]
“Spec patterns,” December 2010, http://patterns.projects.cis.ksu.edu/.
[19]
S. Salamah, A. Gates, S. Roach, and O. Mondragon, “Verifying pattern-generated LTL formulas: a case study,” in Proceedings of the 12th International SPIN Workshop, pp. 200–220, San Francisco, Calif, USA, August 2005.
[20]
“LTL2NBA,” March 2007, http://www.ti.informatik.uni-kiel.de/ABA-Simulation/ltl.cgi.
[21]
O. Mondragon, A. Gates, and S. Roach, “Composite propositions:toward support for formal specification of system properties,” in Proceedings of the 27th Annual IEEE/NASA Goddard Software Engineering Workshop, Greenbelt, Md, USA, December 2002.
