Model Checking Satellite Operational Procedures
Federico Cavaliere, Federico Mari, Igor Melatti, Giovanni Minei, Ivano Salvo, Enrico Tronci, Giovanni Verzino, Yuri Yushtein · 2011
Satellite Operational Procedures (OPs) are mission criti-cal systems which verification typically requires months of simulation. Automating OP verification by using model checking techniques to explore all possible sce-narios will decrease OP verification cost and increase OP reliability. The main obstruction is modeling the satellite inside a model checker. We show how, by using an ex-plicit model checker (CMurphi), it is possible to exploit a satellite simulator (SIMSAT) to automate OP verifica-tion. We model OPs, disturbances as well as the behavior of the human operator by using the model checker mod-eling language and instead use the satellite simulator as a model of the satellite itself. We achieve this by using the model checker as a driver for the simulation activity. In order to assess feasibility of our approach we present experimental results on a simple yet meaningful OP. Our results show that we can save up to 90 % of verification time. Key words: Automatic verification of satellite opera-tional procedures; Model checking; SIMSAT. 1.