Improving Efficiency of Symbolic Model Checking for State-Based System Requirements

from the Research Page of William Chan

Paper by William Chan, Richard J. Anderson, Paul Beame, and David Notkin. In ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 102-112, March 1998, Clearwater Beach, Florida, USA.

Download (11 pages):

Abstract

We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques in our analysis of the system requirements specification of TCAS II, a complex aircraft collision avoidance system. They together reduce the time and space complexities by orders of magnitude, making feasible some analysis that was previously intractable. The TCAS II requirements were written in RSML, a dialect of statecharts.

Keywords

Formal verification, symbolic model checking, reachability analysis, binary decision diagrams, partitioned transition relation, statecharts, RSML, TCAS II, system requirements specification, abstraction.

BibTeX entry

@InProceedings( Chan-ISSTA98,
  title = "Improving Efficiency of Symbolic Model Checking for
           State-Based System Requirements",
  author = "William Chan and Richard J. Anderson and Paul Beame
            and David Notkin",
  booktitle="ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium
             on Software Testing and Analysis",
  month = mar, 
  year = 1998,
  address = "Clearwater Beach, Florida, USA",
  publisher = "ACM",
  editor="Michal Young",
  pages="102--112"
)

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)