TY - JOUR
T1 - From NuSMV to SPIN
T2 - Experiences with model checking flight guidance systems
AU - Choi, Yunja
PY - 2007/6
Y1 - 2007/6
N2 - 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.
AB - 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.
KW - Flight guidance systems
KW - Model checking
KW - NuSMV
KW - SPIN
UR - http://www.scopus.com/inward/record.url?scp=34247101917&partnerID=8YFLogxK
U2 - 10.1007/s10703-006-0027-9
DO - 10.1007/s10703-006-0027-9
M3 - Article
AN - SCOPUS:34247101917
SN - 0925-9856
VL - 30
SP - 199
EP - 216
JO - Formal Methods in System Design
JF - Formal Methods in System Design
IS - 3
ER -