Formal patterns for multi-rate distributed real-time systems

Kyungmin Bae, José Meseguer, Peter Csaba Ölveczky

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

Abstract

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 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)
Title of host publicationFormal Aspects of Component Software - 9th International Symposium, FACS 2012, Revised Selected Papers
Pages1-18
Number of pages18
DOIs
StatePublished - Jan 28 2013
Event9th International Symposium on Formal Aspects of Component Software, FACS 2012 - Mountain View, CA, United States
Duration: Sep 12 2012Sep 14 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7684 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Symposium on Formal Aspects of Component Software, FACS 2012
Country/TerritoryUnited States
CityMountain View, CA
Period9/12/129/14/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

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

Cite this