Formal Methods in System Design

, Volume 30, Issue 3, pp 199–216 | Cite as

From NuSMV to SPIN: Experiences with model checking flight guidance systems

  • Yunja Choi


Model checking has become a promising technique for verifying software and hardware designs; it has been routinely used in hardware verification, and a number of case studies and industrial applications show its effectiveness in software verification as well. Nevertheless, most existing model checkers are specialized for limited aspects of a system, where each of them requires a certain level of expertise to use the tool in the right domain in the right way. Hardly any guideline is available on choosing the right model checker for a particular problem domain, which makes adopting the technique difficult in practice, especially for verifying software with high complexity.

In this work, we investigate the relative pitfalls and benefits of using the explicit model checker Spin on commercial Flight Guidance Systems (FGSs) at Rockwell-Collins, based on the author's prior experience with the use of the symbolic model checker NuSMV on the same systems. This has been a question from the beginning of the project with Rockwell-Collins. The challenge includes the efficient use of Spin for the complex synchronous mode logic with a large number of state variables, where Spin is known to be not particulary efficient. We present the way the Spin model is optimized to avoid the state space explosion problem and discuss the implication of the result. We hope our experience can be a useful 21 reference for the future use of model checking in a similar domain.


Model checking Flight guidance systems SPIN NuSMV 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Avrunin GS, Corbett JC, Dwyer MB (2000) Benchmarking finite-state verifiers. Softw Tools for Technol Transf 2(4):317–320CrossRefGoogle Scholar
  2. 2.
    Chan W, Anderson RJ, Beame P, Burns S, Modugno F, Notkin D, Reese JD (1998) Model checking large software specifications. IEEE Trans Softw Eng 24(7):498–520CrossRefGoogle Scholar
  3. 3.
    Choi Y, Heimdahl M (2002) Model checking RSML−e requirements. In: Proceedings of the 7th IEEE/IEICE international symposium on high assurance systems engineering, pp 109–118Google Scholar
  4. 4.
    Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT PressGoogle Scholar
  5. 5.
    Dong Y, Du X, Holzmann GJ, Smolka SA (2003) Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking. Int J Softw Tools Technol Transf (4)Google Scholar
  6. 6.
    Dong Y, Du X, et al (1999) Fighting livelock in the i-protocol: a comparative study of verification tools. In: Proceedings of TACASGoogle Scholar
  7. 7.
    Eisner C, Peled D (2002) Comparing symbolic and explicit model checking of a software system. In: SPIN WorkshopGoogle Scholar
  8. 8.
    Berry G, Gonthier G (1992) The ESTEREL synchronous programming language: design, semantics, implementation. Sci Comput Programm 19(2):87–152MATHCrossRefGoogle Scholar
  9. 9.
    Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: 17th IEEE international conference on automated software engineering, pp 3–12Google Scholar
  10. 10.
    Goering R (1997) Model checking expands verification’s scope. Electron Eng TodayGoogle Scholar
  11. 11.
    Halbwachs N, Caspi P, Raymond P, Pilaud D (1991) The synchronous dataflow programming language lustre. Proc IEEE 79(9):1305–1320CrossRefGoogle Scholar
  12. 12.
    Hatcliff J, Dwyer MB, Zheng H (2000) Slicing software for model construction. Higher-Order and Symbolic Comput 13(4):315–353Google Scholar
  13. 13.
    Havelund K, Pressburger T (2000) Model checking Java programs using Java pathfinder. Int J Softw Tools Technol Transf 366–381Google Scholar
  14. 14.
    Heimdahl MPE, Whalen M, Thompson J (2003) NIMBUS: A tool for specification centered development. Presented at the 11th IEEE international requirements engineering conferenceGoogle Scholar
  15. 15.
    Heimdahl MPE, Whalen MW (1997) Reduction and slicing of hierarchical state machines. In: Proceedings of the 5th ACM SIGSOFT symposium on the foundations of software engineeringGoogle Scholar
  16. 16.
    Heitmeyer C, Kirby J Jr, Labaw B, Archer M, Bharadwaj R (1998) Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans Softw Eng 24(11):927–948Google Scholar
  17. 17.
    Holzmann GJ (1997) The model checker spin. IEEE Trans Softw Eng 23(5)Google Scholar
  18. 18.
    Holzmann GJ (1999) The engineering of a model checker: the gnu i-protocol case study revisited. In: SPIN workshopGoogle Scholar
  19. 19.
    Holzmann GJ (2003) The SPIN model checker: primer and reference manual. Addison-Wesley Publishing CompanyGoogle Scholar
  20. 20.
    Leveson NG, Heimdahl MPE, Reese JD (1999) Designing specification languages for process control systems: Lessons learned and steps to the future. In: Proceedings of the 7th ACM SIGSOFT symposium on the foundations on software engineering, LNCS, vol 1687, pp 127–145Google Scholar
  21. 21.
    Luettgen G, Carreno V (1999) Analyzing mode confusion via model checking. In: SPIN workshopGoogle Scholar
  22. 22.
    Miller S, Tribble A (2002) A methodology for improving mode awareness in flight guidance design. In: Digital avionics systems conferenceGoogle Scholar
  23. 23.
    Miller SP, Tribble AC, Heimdahl MPE (2003) Proving the shalls. In: Formal methods EuropeGoogle Scholar
  24. 24.
    NuSMV: A New Symbolic Model Checking. Available at Scholar
  25. 25.
    Owre S, Shankar N, Rushby JM (1993) User guide for the PVS specification and verification system. Computer Science Laboratory; SRI International, Menlo Park, CA 94025, beta release editionGoogle Scholar
  26. 26.
    Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium foundations of computer science, pp 46–57Google Scholar
  27. 27.
    Weiser M (1984) Program slicing. IEEE Trans Softw Eng SE-10(4):352–357CrossRefGoogle Scholar
  28. 28.
    Whalen MW (2000) A formal semantics for RSML−e. Master’s thesis, University of MinnesotaGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2006

Authors and Affiliations

  1. 1.School of Electrical Engineering and Computer ScienceKyungpook National UniversityDaeguSouth Korea

Personalised recommendations