Using System Analysis Modeling Language (SAML) for validating the critical aerospace model.

System Analysis Modeling Language (SAML) is a formal language which helps in expressing and analyzing the qualitative and quantitative aspects of the software as well as hardware models. This can be used in model-based safety analysis (MBSA) which provides the means of identifying, localizing and analyzing hazards in these real-time Safety-Critical Systems. This paper describes the work carried out in the organization to validate the complex and critical Mode-Transition Logic (MTL) in Automated Flight Control System (AFCS) being developed in the organization. The Mode-Transition Logic (MTL) of the AFCS system is re-modeled using SAML and further analyzed with model checkers such as PRISM and NuSMV, for generation of counter-examples. The counter examples helped in mapping the safety scenarios along the AFCS requirements. These counter examples also helped in generating the fault model and analyzing the system logic for fault tolerance. Using NUSMV, MTL the failure scenarios were generated and the allowed transitions were studied. Failure management analysis report is generated and mapped as an artefact for the certification. For the illustration of the proposed approach, a suitable framework viz. Verification Environment for Safety-Critical Systems (VECS) is used to validate the utility of Mode-Transition Logic (MTL) in Automated Flight Control System (AFCS). The critical operations and complex functions were analyzed for contingency situations and provide means in significantly enhancing the safe operation of the Safety-Critical System. The mapping of the model safety using this approach will provide compliance with Civil Aerospace Standard DO-178C and DO-331 using Model-Based Design