Formal patterns for multirate distributed real-time systems

Kyungmin Bae, José Meseguer, Peter Csaba Ölveczky

Research output: Contribution to journalArticlepeer-review


Distributed real-time systems (DRTSs), such as avionics and automotive systems, are very hard to design and verify. Besides the difficulties of asynchrony, clock skews, and network delays, an additional source of complexity comes from the multirate nature of many such systems, which must implement several levels of hierarchical control at different rates. In previous work we showed how the design and implementation of a single-rate DRTS which should behave in a virtually synchronous way can be drastically simplified by the PALS model transformation that generates the DRTS from a much simpler synchronous model. In this work we present several simple model transformations and a multirate extension of the PALS pattern which can be combined to reduce the design and verification of a virtually synchronous multirate DRTS to the much simpler task of specifying and verifying a single synchronous system. We illustrate the ideas with a multirate hierarchical control system where a central controller orchestrates control systems in the ailerons and tail of an airplane to perform turning maneuvers.

Original languageEnglish (US)
Pages (from-to)3-44
Number of pages42
JournalScience of Computer Programming
Issue numberPART A
StatePublished - Oct 1 2014


  • Distributed real-time systems
  • Model checking
  • Multirate systems
  • Rewriting logic
  • Synchronizers

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Formal patterns for multirate distributed real-time systems'. Together they form a unique fingerprint.

Cite this