Behavioral analysis of Safety Critical Systems using formal methods

Structural analysis in Software Engineering hinders the colossal aspects of architecture and functional behavior of the systems. The analysis of the same yields in flow oriented view of the blocks involved, rather than their functional behavior. Thus a need to analyze the behavior of systems, leads us to a newer approach called behavior analysis. The ever increasing complexity of Safety Critical Systems is driving us towards the usage of formal methods that facilitates in building systems less expensively, more rapidly and predictively at early stages of software design life cycle. A formal language used in this approach is Architecture Analysis & Design Language (AADL), which is an International Standard, supporting the analysis of the system attributes such as safety, security, responsiveness through model annotations. In this paper, we propose an analytical approach to validate the architecture of Safety Critical System using an acclaimed formal method, AADL. The efficacy of `Architecture Based approach´ as opposed to `Design Based approach´ is established by considering a case study of the proven Safety Critical System, Automatic Flight Control System (AFCS).