Model Checking Flight Guidance Systems: from Synchrony to Asynchrony

Based on the author's prior experience with the use of the symbolic model checker NuSMV on commercial Flight Guidance Systems (FGS) at Rockwell-Collins, the relative benefits and pitfalls of using the explicit model checker SPIN on the same problem are investigated. This has been a question from the beginning of the project with Rockwell-Collins. The challenge includes an 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, which makes SPIN scale up better than NuSMV in the end, and discuss the implication of the result. We hope our experience can be a useful reference for the future use of model checking in a similar domain.