Formal Specification of the ARINC 653 Architecture Using Circus

Nowadays, the avionics industry is moving towards the use of a new architecture for aircraft systems called Integrated Modular Avionics (IMA), which consists of a distributed, highly integrated platform, in which a variety of applications can be executed in the same hardware. Standards and guidelines for the development of aircraft systems now provide guidance for using formal methods during the development process of these systems. In this dissertation we present an approach for using Circus as a formal language to model and validate the IMA architecture focusing on temporal partitioning. We provide here an overview of the IMA architecture, detailing its components and features. We also present an overview of existing approaches on certification and verification of IMA systems. We also present a brief survey of formal languages for the design of concurrent systems. Later, we present a Circus model of three layers of components of the IMA architecture. It comprises a model of the operating system layer, the application executive (APEX) layer and the partitions layer. Moreover, we validate the Circus model by translating it into CSP with time constructs and using the model checker FDR. Finally, we conclude this dissertation with our plans for future work.