Towards Support for Software Model Checking : Improving the Efficiency of Formal Specifications
Joint Authors
Roach, Steve
Salamah, Salamah
Engskow, Matthew
Gates, Ann Q.
Source
Advances in Software Engineering
Issue
Vol. 2011, Issue 2011 (31 Dec. 2011), pp.1-13, 13 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2011-06-22
Country of Publication
Egypt
No. of Pages
13
Main Subjects
Abstract EN
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.
American Psychological Association (APA)
Salamah, Salamah& Gates, Ann Q.& Roach, Steve& Engskow, Matthew. 2011. Towards Support for Software Model Checking : Improving the Efficiency of Formal Specifications. Advances in Software Engineering،Vol. 2011, no. 2011, pp.1-13.
https://search.emarefa.net/detail/BIM-504810
Modern Language Association (MLA)
Salamah, Salamah…[et al.]. Towards Support for Software Model Checking : Improving the Efficiency of Formal Specifications. Advances in Software Engineering No. 2011 (2011), pp.1-13.
https://search.emarefa.net/detail/BIM-504810
American Medical Association (AMA)
Salamah, Salamah& Gates, Ann Q.& Roach, Steve& Engskow, Matthew. Towards Support for Software Model Checking : Improving the Efficiency of Formal Specifications. Advances in Software Engineering. 2011. Vol. 2011, no. 2011, pp.1-13.
https://search.emarefa.net/detail/BIM-504810
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-504810