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

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 fo- TTA that was developed 15 years ago, thereby illustrating that a mechanized formal analysis is an intellectual investment that supports cost-effective reuse.