Symbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbolic modal checking for systems specified as statecharts. We used these techniques in our analyses of the models of a collision avoidance system and a fault-tolerant electrical power distribution (EPD) system, both used on commercial aircraft. The techniques together reduce the time and space requirements by orders of magnitude, making feasible some analysis that was previously intractable. We also elaborate on the results of verifying the EPD model. The analysis disclosed subtle modeling and logical flaws not found by simulation.

Article Free Access Share on Decoupling synchronization from local control for efficient symbolic model checking of statecharts Authors: William Chan Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , Richard J. Anderson Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , Paul Beame Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , David H. Jones The Boeing Company, Seattle, Washington The Boeing Company, Seattle, WashingtonView Profile , David Notkin Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , William E. Warner The Boeing Company, Seattle, Washington The Boeing Company, Seattle, WashingtonView Profile Authors Info & Claims ICSE '99: Proceedings of the 21st international conference on Software engineeringMay 1999 Pages 142–151https://doi.org/10.1145/302405.302460Online:16 May 1999Publication History 13citation235DownloadsMetricsTotal Citations13Total Downloads235Last 12 Months7Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

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 state-charts.

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 symbolic model checker (SMV). We successfully used the symbolic 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.

In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in the question of whether or not model checking techniques can be applied to large software specifications.To investigate this, we translated a portion of the finite-state requirements specification of TCAS II (Traffic Alert and Collision Avoidance System) into a form accepted by a model checker (SMV). We successfully used the model checker to investigate a number of dynamic properties of the system.We report on our experiences, describing our approach to translating the specification to the SMV language and our methods for achieving acceptable performance in model checking, and giving a summary of the properties that we were able to check. We consider the paper as a data point that provides reason for optimism about the potential for successful application of model checking to software systems. In addition, our experiences provide a basis for characterizing features that would be especially suitable for model checkers built specifically for analyzing software systems.The intent of this paper is to evaluate symbolic model checking of state-machine based specifications, not to evaluate the TCAS II specification. We used a preliminary version of the specification, the version 6.00, dated March, 1993, in our study. We did not have access to later versions, so we do not know if the properties identified here are present in later versions.