Analysing MTL Properties using NuSMV model checker

Reliability and safety property of any hardware is an important parameter. To achieve this and to improve the performance bounds of the designed system it is important to enhance the efficiency by proper verification techniques. To overcome the problems arising due to the software crisis, formal methods are used. The use of formal methods in aerospace domain is the latest research that is being carried out. Formal verification, a part of formal methods is a mathematical modelling technique used to verify the hardware systems. Technique such as model checking is used to efficiently bridge the gap between design and developed stage of the system with less errors and more efficiency. In this paper, we propose to use NuSMV for verifying the vertical mode functionality of the Mode Transition Logic (MTL). MTL is a very critical functionality in aircraft. It assists the control of trajectories, weather and systems. The NuSMV model checker is used to analyse the functional behaviour of the model. The model is initially designed and developed using Mat-lab/Simulink tool suite. The semantic translation of the MTL model to NuSMV is done by means of specification languages such as CTL and LTL. Test cases generated at the Simulink model level are used as a reference to test the linear and non-linear properties of the MTL vertical model in NuSMV. These test cases are compared with the results obtained using NuSMV analysis. The efficiency is defined by earlier fault detection and improving the software development life cycle of the system