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