Modern defense systems are complex distributed software systems implemented over heterogeneous and constantly evolving hardware and software platforms. Distributed agreement protocols are often developed exploiting the fact that their systems are quasi-synchronous, where even though the clocks of the different nodes are not synchronized, they all run at the same rate, or multiples of the same rate, modulo their drift and jitter. This paper describes an effort to provide systems designers and engineers with an intuitive modeling environment that allows them to specify the highlevel architecture and synchronization logic of quasi-synchronous systems using widely available systemsengineering notations and tools. To this end, a translator was developed that translates system architectural models specified in a subset of SysML into the Architectural Analysis and Description Language (AADL). Translators were also developed that translate the AADL models into the input language of the Uppaal and Kind model checkers. The Uppaal model checker. supports the modeling, verification, and validation of real-time systems modeled as a network of timed automata. This paper focuses on the challenges encountered in translating from AADL to Uppaal, and illustrates the overall approach with a common avionics example: the Pilot Flying System.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Verification of quasi-synchronous systems with Uppaal


    Beteiligte:
    Bhattacharyya, S. (Autor:in) / Miller, S. (Autor:in) / Yang, J. (Autor:in) / Smolka, S. (Autor:in) / Meng, B. (Autor:in) / Sticksel, C. (Autor:in) / Tinelli, C. (Autor:in)


    Erscheinungsdatum :

    2014-10-01


    Format / Umfang :

    477721 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Verification of quasi-synchronous systems with Uppaal

    Bhattacharyya, Siddhartha Sid | IEEE | 2014


    Schedulability Analysis of Distributed Multicore Avionics Systems with UPPAAL

    Han, Pujie / Zhai, Zhengjun / Nielsen, Brian et al. | AIAA | 2019


    Online and Proactive Vehicle Rerouting with Uppaal Stratego

    Bilgram, Alexander / Ernstsen, Emil / Greve, Peter et al. | Transportation Research Record | 2021


    Formal Development of Multi-vessel Navigation of Maritime Autonomous Systems using UPPAAL STRATEGO

    Shokri-Manninen, Fatima / Vain, Jüri / Waldén, Marina | BASE | 2021

    Freier Zugriff