Experiences with the application of symbolic model checking to the analysis of symbolic model checking to the analysis of software specifications

摘要

Symboilic model checking is a powerful formal-verification technique which has been used to analyze many hardware systems. In this paper we present our experimences in applying symbolic model checking to software specifications of reactive systems. We have conducted two in depth case studies: one, using the specification of TCAS II (Traffic Alert and Collision Avoidance System II), and the other using a model of an aircraft electrical system. Based on these case studies, we have gained significant experience in how model checking can be used in to analyze software specificatioins, and have also overcome a number of performance bottlenecks to make the analysis tractable.