Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications. (22nd June 2011)

• Record Type: Journal Article
• Authors: Salamah, Salamah; Gates, Ann Q.; Roach, Steve; Engskow, Matthew
• Other Names: Laplante Phillip Academic Editor.
• Is Part Of: Advances in software engineering. Volume 2011(2011)
• Publication Date: 2011-06-22
• Subjects: Software engineering -- Periodicals; Software engineering; Periodicals; Electronic journals; 005.1
• DOI: 10.1155/2011/869182
• Languages: English
• ISSNs: 1687-8655

Abstract

Abstract : 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.