TTA and PALS: Formally Verified Design Patterns for Distributed Cyber-Physical Systems

Wilfried Steiner, TTTech Computertechnik AG, Vienna Austria
John Rushby, SRI International, Menlo Park CA USA

Presented at the 30th IEEE/AIAA Digital Avionics Systems Conference (DASC), Seattle WA, October 2011.

Recipient of "Best in Session" and "Best in Track" awards.


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.




BibTeX Entry

TBD (proceedings not yet available)

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page