The aviation industry is gradually moving toward the use of integrated modular avionics (IMA) for civilian transport aircraft. We have investigated the problem of ensuring safe partitioning and logical non-interference among separate applications running on a shared Avionics Computer Resource (ACR). This research was performed in the context of ongoing standardization efforts, in particular, the work of RTCA committee SC-182, and the recently completed ARINC 653 application executive (APEX) interface standard. We have developed a formal model of partitioning suitable for evaluating the design of an ACR. The model draws from the mathematical modeling techniques developed by the computer security community. This report presents a formulation of partitioning requirements expressed first using conventional mathematical notation, then formalized using the language of SRI'S Prototype Verification System (PVS). The approach is demonstrated on three candidate designs, each an abstraction of features found in real systems.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Formal Model of Partitioning for Integrated Modular Avionics


    Contributors:

    Publication date :

    1998


    Size :

    90 pages


    Type of media :

    Report


    Type of material :

    No indication


    Language :

    English





    Integrated modular avionics

    Prisaznuk, P.J. | IEEE | 1992


    Using Model Checking for Verification of Partitioning Properties in Integrated Modular Avionics

    Cofer, D. / IEEE / AIAA | British Library Conference Proceedings | 2000


    Integrated Modular Avionics System Design Based on Formal Dynamic Organization

    Wang, Miao / Xiao, Gang / Liu, Xiaoqin et al. | IEEE | 2019