Model checking large software specifications
from the Research Page of William Chan
Paper by
William Chan,
Richard J. Anderson,
Paul Beame,
Steve Burns,
Francesmary Modugno,
David Notkin,
and
Jon D. Reese.
In
IEEE Transactions on Software Engineering 24(7),
pages 498-520, July 1998.
Conference version appeared in
SIGSOFT'96: Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundation of
Software Engineering,
pages 156-166, October 1996, San Francisco, USA.
Download (25 pages):
Errata for the published article in TSE (2 pages):
Abstract
In this paper we present our experiences in using symbolic
model checking to analyze a specification of
a software system for aircraft collision avoidance.
Symbolic model checking has been highly successful
when applied to hardware systems. We are interested in
whether model checking can be effectively applied to large
software specifications.
To investigate this, we translated a portion of the state-based system
requirements specification of
Traffic Alert and Collision Avoidance System II
(TCAS II)
into input to a model checker (SMV). We
successfully used the model checker to analyze a number of
properties of the system.
We report on our experiences, describing our approach to translating
the specification to the SMV language,
explaining our methods for achieving acceptable performance,
and giving a summary of the properties analyzed.
Based on our experiences,
we discuss the possibility of using model checking to
aid specification development
by iteratively applying the technique early in the development cycle.
We consider the paper to be a data point
for optimism about the potential for more widespread
application of model checking to software systems.
BibTeX entry
@article( Chan-TSE98,
title = "Model Checking Large Software Specifications",
author = "William Chan and Richard J. Anderson and Paul Beame and
Steve Burns and Francesmary Modugno and David Notkin and
Jon D. Reese",
journal = "IEEE Transactions on Software Engineering",
year = 1998,
month = jul,
volume = 24,
number = 7,
pages = "498--520",
)
William Chan
(wchan@cs.washington.edu)