A formal architecture pattern for real-time distributed systems

Abdullah Al-Nayeem, Mu Sun, Xiaokang Qiu, Lui Raymond Sha, Steven P. Miller, Darren D. Cofer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Pattern solutions [1] for software and architectures have significantly reduced design, verification, and validation times by mapping challenging problems into a solved generic problem. In the paper, we present an architecture pattern for ensuring synchronous computation semantics using the PALS protocol [2]. We develop a modeling framework in AADL to automatically transform a synchronous design of a real-time distributed system into an asynchronous design satisfying the PALS protocol. We present a detailed example of how the PALS transformation works for a dual-redundant system. From the example, we also describe the general transformation in terms of intuitively defined AADL semantics. Furthermore, we develop a static analysis checker to find necessary conditions that must be satisfied in order for the PALS transformation to work correctly. The transformations and static checks that we have described are implemented in OSATE using the generated EMF metamodel API for model manipulation.

Original languageEnglish (US)
Title of host publicationProceedings - Real-Time Systems Symposium, RTSS 2009
Number of pages10
StatePublished - 2009
EventReal-Time Systems Symposium, RTSS 2009 - Washington, D.C., United States
Duration: Dec 1 2009Dec 4 2009

Publication series

NameProceedings - Real-Time Systems Symposium
ISSN (Print)1052-8725


OtherReal-Time Systems Symposium, RTSS 2009
Country/TerritoryUnited States
CityWashington, D.C.


  • Architecture description language
  • Architecture pattern
  • Formal verification
  • GALS
  • Logical synchronization

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications


Dive into the research topics of 'A formal architecture pattern for real-time distributed systems'. Together they form a unique fingerprint.

Cite this