Arguing formally about flight control laws using SLDV and NUSMV

Abstract

Software systems have failed in the recent past. This is most often attributed to wrong requirements often caught very late in the program or escapes from the rigorous process leading to failures. There is a necessity to ensure that the requirements are correct up front before the design and verification process start. Formal methods have become popular these days and a lot of impetus is there in the industry to apply these techniques to safety critical projects especially in flight controls. This paper looks at two tools NuSMV, an open source model checker, and Simulink Design Verifier, a commercial model checker. It is seen that these can be practically applied to projects and design. These are very successful in finding defects in design and requirements as demonstrated on a set of mutants. © Springer Nature Singapore Pte Ltd. 2018. All rights reserved.