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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2013

Author dc:creator

• Al-Nayeem, Abdullah

Contributors dc:contributor

• Sha, Lui R.
• Caccamo, Marco
• Mitra, Sayan
• Cofer, Darren D.

• Logical synchronization in real-time distributed systems
• Formal architectural pattern
• Complexity-reduction
• Cyber-physical systems

Statement dc:rights

• Copyright 2013 Abdullah Al-Nayeem This dissertation is partially based on the materials previously published in following peer-reviewed conference papers. They are reprinted with permission. 1. Abdullah Al-Nayeem, Mu Sun, Xiaokang Qiu, Lui Sha, Steven P. Miller, and Darren D. Cofer, “A Formal Architecture Pattern for Real-Time Distributed Systems”, Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS), pp. 161-170, 1-4 Dec. 2009, Copyright 2009 IEEE. 2. Abdullah Al-Nayeem, Lui Sha, Darren D. Cofer, and Steven P. Miller, “Pattern-Based Composition and Analysis of Virtually Synchronized Real-Time Distributed Systems”, Proceedings of the 3rd IEEE/ACM International Conference on Cyber-Physical Systems (ICCPS), pp. 65-74, 17-19 April 2012, Copyright 2012 IEEE. 3. Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem, and Jose Meseguer, “Synchronous AADL and Its Formal Analysis in Real-Time Maude”, Proceedings of the 13th International Conference on Formal Methods and Software Engineering, pp. 651-667, 22 Oct. 2011, Copyright 2011 Springer Berlin / Heidelberg. 4. Steven Miller, Darren Cofer, Lui Sha, Jose Mesguer, and Abdullah Al-Nayeem, “Implementing Logical Synchrony in Integrated Modular Avionics”, Proceedings of the 28th IEEE/AIAA Digital Avionics Systems Conference, pp. 1.A.3-1-1.A.3-12, 23-29 Oct. 2009, Copyright 2009 IEEE.

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/45438

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/45438