Decoupling Synchronization from Local Control for Efficient Symbolic Model Checking of Statecharts

from the Research Page of William Chan

Paper by William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, and William E. Warner. In Proceedings of the 1999 International Conference on Software Engineering (ICSE'99), pages 142-151, May 1999, Los Angeles, USA.

Download (10 pages):

Abstract

Symbolic model checking is a powerful formal-verification technique for reactive systems. In this paper we address the problem of symbolic model checking for software specifications written as statecharts. We concentrate on how the synchronization of statecharts relates to the efficiency of model checking. We show that statecharts synchronized in an oblivious manner, such that the synchronization and the local control are decoupled, tend to be easier for symbolic analysis. Based on this insight, the verification of some non-oblivious systems can be optimized by a simple, transparent modification to the model to separate the synchronization from the local control. The technique enabled the analysis of the statecharts model of a fault-tolerant electrical power distribution system developed by the Boeing Commercial Airplane Group. The results disclosed subtle modeling and logical flaws not found by simulation.

Keywords

Formal methods, formal verification, symbolic model checking, binary decision diagrams, software specification, statecharts, fault tolerance.

BibTeX entry

@inproceedings( Chan-ICSE99,
  title = "Decoupling Synchronization from Local Control for Efficient Symbolic Model Checking of Statecharts",
  author = "William Chan and Richard J. Anderson and Paul Beame and David H. Jones and David Notkin and William E. Warner",
  booktitle="Proceedings of the 1999 International Conference on Software Engineering: ICSE 99",
  address="Los Angeles, USA",
  month = may, 
  year = 1999,
  pages = "142--151"
)

The documents distributed here have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by the copyright of each author. These works may not be reposted without the explicit permission of the copyright holder.

William Chan (wchan@cs.washington.edu)