Physically-asynchronous logically-synchronous (PALS) system design and development

Cyber-physical systems, such as avionics and automobiles, are real-time distributed systems, where many of the information processing functions require consistent views and actions across distributed computing nodes. Guaranteeing consistency in these distributed computations is challenging. In particular, distributed systems are physically asynchronous because system clocks at each node cannot be perfectly synchronized. Such physical asynchrony, if not properly dealt with, can lead to distributed race conditions and subsequently result in inconsistent actions and anomalous system behaviors. In this thesis, we address this problem and introduce a novel design methodology that guarantees consistency in real-time distributed computations. At the core of this approach is a complexity-reducing architectural pattern, called the Physically-Asynchronous Logically-Synchronous (PALS) system. The PALS system is a formal architectural pattern that engineers can use to develop distributed applications as if they would operate on a globally synchronous architecture with a single global clock. The pattern maps the globally synchronous design as a logically synchronous design executing on the physically asynchronous architecture. It provides significant benefit in terms of the verification of safety and correctness. The formal verification cost is greatly reduced since engineers only verify the simple globally synchronous model. The thesis makes several contributions to the design and development of the PALS system: C1 - Architectural model definitions: We propose architectural model definitions of the globally synchronous design and its equivalent logically synchronous design using SAE Architecture Analysis and Design Language (AADL), an industry-standard modeling language. C2 - Formal pattern specification and analysis: One of the biggest challenges in model-based engineering is to preserve the verification properties as engineers refine and extend the models during the development process. We therefore give a formal specification of this pattern and perform static analysis to detect any error during the system design. C3 - Multi-rate PALS system: We extend the PALS system to support multi-rate distributed computations. We provide an architectural analysis to support composition of multiple instances of this pattern in a given system model. C4 - Middleware design for PALS system: We have developed a middleware to implement the PALS applications in C++. The middleware addresses several implementation challenges, e.g. node failure, integration with underlying infrastructure components