Definition, semantics, and analysis of multirate synchronous AADL

Kyungmin Bae, Peter Csaba Ölveczky, José Meseguer

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

Abstract

Many cyber-physical systems are hierarchical distributed control systems whose components operate with different rates, and that should behave in a virtually synchronous way. Designing such systems is hard due to asynchrony, skews of the local clocks, and network delays; furthermore, their model checking is typically unfeasible due to state space explosion. Multirate PALS reduces the problem of designing and verifying virtually synchronous multirate systems to the much simpler tasks of specifying and verifying their underlying synchronous design. To make the Multirate PALS design and verification methodology available within an industrial modeling environment, we define in this paper the modeling language Multirate Synchronous AADL, which can be used to specify multirate synchronous designs using the AADL modeling standard. We then define the formal semantics of Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification into the OSATE tool environment for AADL. Finally, we show how an algorithm for smoothly turning an airplane can be modeled and analyzed using Multirate Synchronous AADL.

Original languageEnglish (US)
Title of host publicationFM 2014
Subtitle of host publicationFormal Methods - 19th International Symposium, Proceedings
PublisherSpringer-Verlag
Pages94-109
Number of pages16
ISBN (Print)9783319064093
DOIs
StatePublished - Jan 1 2014
Event19th International Symposium on Formal Methods, FM 2014 - Singapore, Singapore
Duration: May 12 2014May 16 2014

Publication series

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

Other

Other19th International Symposium on Formal Methods, FM 2014
CountrySingapore
CitySingapore
Period5/12/145/16/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Definition, semantics, and analysis of multirate synchronous AADL'. Together they form a unique fingerprint.

Cite this