Recipient of "Best in Session" and "Best in Track" awards.
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.
PDF
TBD (proceedings not yet available)