This paper presents an approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 multicore modules connected by a unified Avionics Full-Duplex Switched Ethernet (AFDX) network. A multicore DIMA system is modeled as a set of stopwatch automata in uppaal to verify its schedulability by model checking. However, direct verification is infeasible due to the large state space. Therefore, global analysis based on statistical model checking (SMC) and compositional analysis based on classical model checking are combined, thereby mitigating the state space explosion problem. Even though the nature of SMC testing cannot prove schedulability, the model of a DIMA system first undergoes quick schedulability falsification using global SMC analysis. Thereafter, a compositional approach is used to check each partition, including its communication environment individually. By using assume-guarantee reasoning, it is ensured that each real-time task meets the deadline and that communication constraints are also fulfilled globally. The approach is finally applied to the schedulability analysis of a concrete multicore DIMA system.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Schedulability Analysis of Distributed Multicore Avionics Systems with UPPAAL


    Beteiligte:
    Han, Pujie (Autor:in) / Zhai, Zhengjun (Autor:in) / Nielsen, Brian (Autor:in) / Nyman, Ulrik (Autor:in) / Kristjansen, Martin (Autor:in)

    Erschienen in:

    Erscheinungsdatum :

    2019-10-22


    Format / Umfang :

    27 pages




    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Empirical Bounds of Multicore Cache Interference for Real-Time Schedulability Analysis

    Srinivasan, Srini / Kegley, Russell / Gerhardt, Mark et al. | IEEE | 2019


    Verification of quasi-synchronous systems with Uppaal

    Bhattacharyya, S. / Miller, S. / Yang, J. et al. | IEEE | 2014


    Verification of quasi-synchronous systems with Uppaal

    Bhattacharyya, Siddhartha Sid | IEEE | 2014


    COTS Multicore Processors in Avionics Systems: Challenges and Solutions

    de Niz, Dionisio / Andersson, Bjorn / Wrage, Lutz | AIAA | 2015