Arguing formally about flight control laws

Flight control law software have errors. Some are found during the extensive testing and certification process and others pass through causing accidents. The testing of flight control software indicates that the code and the model match. But it is very difficult to ensure if the model was correct in the first place. Model checkers like Mathworks Simulink Design Verifier check the models against formally defined conditions and system behavior. The tool can come up with counterexamples that can fail an assertion or proof. A study is done on how easy or difficult it is to teach engineering students this formal process. The problem statement, the Simulink models and the outcome of the study in terms of advantages and disadvantages of using Simulink Design Verifier is highlighted in this preliminary study.