Formal change impact analyses of extended finite state machines using a theorem prover

Bo Guo, Mahadevan Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - 6th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008
Pages335-344
Number of pages10
DOIs
StatePublished - 2008
Event6th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008 - Cape Town, South Africa
Duration: Nov 10 2008Nov 14 2008

Publication series

NameProceedings - 6th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008

Conference

Conference6th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008
Country/TerritorySouth Africa
CityCape Town
Period11/10/0811/14/08

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Software

Fingerprint

Dive into the research topics of 'Formal change impact analyses of extended finite state machines using a theorem prover'. Together they form a unique fingerprint.

Cite this