Avionics systems in modern and next-generation airborne vehicles combine and integrate various real- time applications to efficiently share the physical resources on board. Many of these real-time applications also need to fulfill fault-tolerance requirements-i.e., the applications have to provide a sufficient level of service even in presence of failures-and this combination of real-time and fault- tolerance requirements elevates avionics to a class of cyber-physical systems of the highest complexity. Consequently, avionics design is challenging for avionics architects and application engineers alike. One way to manage complexity is a division of the overall problem into a hierarchical set of layers connected by well-defined interfaces. The avionics architect may then select the fundamental network architecture, like AFDX, TTP or TTEthernet, and hide their idiosyncrasies-in particular, those concerning the way in which time is managed and presented-by providing a more uniform conceptual interface to the application engineer. In this paper we call this interface the "model of computation" and discuss the well-known synchronous model of computation and small extensions thereof for real- time systems. The bridge between the network architecture and the model of computation concerns the way in which distributed real-time applications are organized and it is achieved through "design patterns." We revise and formally analyze two such design patterns, the Sparse Timebase of the Time- Triggered Architecture (TTA) and the Physically- Asynchronous Logically-Synchronous (PALS) approach. Perhaps surprisingly, we show that both design patterns rely on the same assumptions about the network architecture; hence, the choice of network architecture and design pattern should depend on pragmatics and formal considerations orthogonal to those required to support a particular model of computation. Our formal analysis builds directly on the verification in PVS of a PALS-like pattern for TTA that was developed 15 years ago, thereby illustrating that a mechanized formal analysis is an intellectual investment that supports cost-effective reuse.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    TTA and PALS: Formally verified design patterns for distributed cyber-physical systems


    Beteiligte:
    Steiner, Wilfried (Autor:in) / Rushby, John (Autor:in)


    Erscheinungsdatum :

    2011-10-01


    Format / Umfang :

    349726 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified

    S. M. Loos / A. Platzer / L. Nistor | NTIS | 2011


    Efficiency analysis of formally verified adaptive cruise controllers

    Loos, Sarah M. / Witmer, David / Steenkiste, Peter et al. | IEEE | 2013


    Software safety architecture that can be formally verified

    Cossy,M. / STZ Softwaretechnik,DE | Kraftfahrwesen | 2004


    A Deployment Framework for Formally Verified Human-Robot Interactions

    Lestingi, Livia / Askarpour, Mehrnoosh / Bersani, Marcello M. et al. | BASE | 2021

    Freier Zugriff