Effective Extraction of State Invariant for Software Verification

摘要

In software design of complex systems, more time and effort are spent on verification than on constructions. Model checking for software verification techniques offer a large potential to obtain and early integration of verification in the design process. This paper describes how to easily specify and the software properties and to understand the software generating automatically invariant. In this paper deal with issue that state invariant is a property that holds in every reachable state. Not only can be used in understanding and analysis of complex software systems. In addition, it can be used for system verifications such as checking safety, consistency, and completeness. For these reasons, there are many vital researches for deriving state invariant from finite state machine models. In this research was to be considered to extract state invariant. Thus it is likely to be too complex for the user to understand. This paper let the user focus on some interested parts (called scopes) rather than a whole state space in a model. Computation Tree Logic (CTL) is used to specify scopes in which he/she is interested. Given a scope in CTL, forward reachability analysis is used to find out a set of states inside it. Obviously, a set of states calculated in this way is a subset of every reachable state.