White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Formal Specification of the ARINC 653 Architecture Using Circus

Oliveira Gomes, Artur (2012) Formal Specification of the ARINC 653 Architecture Using Circus. MSc by research thesis, University of York.

[img]
Preview
Text (MSc by Research thesis)
circus.pdf

Download (1034Kb)

Abstract

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.

Item Type: Thesis (MSc by research)
Academic Units: The University of York > Computer Science (York)
Depositing User: Mr Artur Oliveira Gomes
Date Deposited: 14 Aug 2012 11:13
Last Modified: 08 Aug 2013 08:49
URI: http://etheses.whiterose.ac.uk/id/eprint/2683

Actions (repository staff only: login required)