Consistency Checks of System Properties Using LTL and Buchi Automata

Formal approaches to software assurance such as model checking and theorem proving aim to improve system dependability. However, software development professionals have not widely adopted these approaches. A major reason for the hesitance is the lack of maturity of tools that can support the use of formal specification approaches. These techniques verify system correctness against formal specifications. Tools such as the Specification Pattern System (SPS) and the Property Specification tool (Prospec) assist users in specifying system properties, which are derived from requirements, into formal specifications in languages such as Linear Temporal Logic (LTL). The goal of such tools is to aid in the generation of a large set of formal specifications of systems. A major advantage of formal specifications is their ability to discover inconsistencies among the generated properties. This research effort has defined an approach to extend the work of the aforementioned Prospec tool to allow for automatic checking of generated system properties for inconsistencies. The approach will facilitate the discovery of discrepancies among system requirements at early stages of system development, providing a return on investment for specifying formal properties with the Prospec tool.