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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Formal Model of Partitioning for Integrated Modular Avionics


    Beteiligte:
    B. L. DiVito (Autor:in)

    Erscheinungsdatum :

    1998


    Format / Umfang :

    90 pages


    Medientyp :

    Report


    Format :

    Keine Angabe


    Sprache :

    Englisch





    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