Verification of aircraft control algorithm at the model level is a challenge. Formal methods play a critical role in mathematically analysing the functionality and completeness of the algorithm. The advantage of using formal method is that it helps in mathematical analysis of complex algorithms for the correctness and guarantees the properties of a particular model using formal verifiers. The project entails the development of a workflow which verifies the correctness of a safety critical embedded system. The workflow is proven by implementing the Mode Transition Logic (MTL) for Autopilot and Stall Warning System model, taken as a case study. The proposed workflow provides a seamless syntactic translation of Simulink Model(s) into probabilistic models with Markov properties, for PRISM Model Checker. This will help in re-assuring the integrity of the model, an integrated module of safety critical systems among various applications such as Aerospace, Automobile, Medical, and Industrial domain.
Validation of control algorithm using formal methods: Validation of mode transition logic of AFCS in SARAS aircraft
2017-03-01
2423876 byte
Conference paper
Electronic Resource
English
SAE Technical Papers | 1981
|Application of Fuzzy Logic to Rotorcraft AFCS
British Library Conference Proceedings | 1993
|A study of (AFCS) communications measurement program
Tema Archive | 1973
|