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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Model checking large software specifications


    Contributors:
    Chan, W. (author) / Anderson, R.J. (author) / Beame, P. (author) / Burns, S. (author) / Modugno, F. (author) / Notkin, D. (author) / Reese, J.D. (author)


    Publication date :

    1997


    Size :

    23 Seiten, 56 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Domain Checking Z Specifications

    Saaltink, M. / United States; National Aeronautics and Space Administration | British Library Conference Proceedings | 1997


    Software model checking for avionics systems

    Cofer, Darren / Whalen, Michael / Miller, Steven | IEEE | 2008


    Applying software model checking to PALS systems

    Nam, Min Young / Chaki, Sagar / Sha, Lui et al. | IEEE | 2014


    Tailoring software acquisition specifications

    Morrey, J.C. / Petrovay, G.O. | Tema Archive | 1976


    Self-checking software

    Cha, Sung D. / Leveson, Nancy G. / Shimeall, Timothy J. et al. | NTRS | 1986