Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover

This paper describes a formal change impact analysis approach for systematic evolution of communicating systems. Systems are modeled using a network of communicating extended finite state machines (CEFSMs) with variables ranging over commonly used data types including numbers, Booleans, arrays, and object fields. Parameterized messages exchanged over queues and shared variables are used for communication. Changes to the system are performed at the transition level by adding/deleting transitions. Given a changed transition, the impacted system transitions are automatically computed using a bounded, selective, state exploration based on the inductive assertion approach. A theorem prover extended with queue axioms is used to discharge the verification conditions. Multiple symbolic values for each variable present in a system state are represented as a set of rewrite rules to minimize state space overheads. Rewrite-rule based procedures are described for reducing the number of symbolic values in system states. We also describe heuristics to identify simultaneously enabled and disabling transitions and describe a procedure to reduce the number of verification conditions generated during the impact analysis. The effectiveness of the proposed approach is illustrated on several applications including Web services and cache coherence protocols.