Synchronous AADL and its formal analysis in real-time maude

Kyungmin Bae, Peter Csaba Ölveczky, Abdullah Al-Nayeem, José Meseguer

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

Abstract

Distributed Real-Time Systems (DRTS), such as avionics systems and distributed control systems in motor vehicles, are very hard to design because of asynchronous communication, network delays, and clock skews. Furthermore, their model checking problem typically becomes unfeasible due to the large state spaces caused by the interleavings. For many DRTSs, we can use the PALS methodology to reduce the problem of designing and verifying asynchronous DRTSs to the much simpler task of designing and verifying their synchronous versions. AADL is an industrial modeling standard for avionics and automotive systems. We define in this paper the Synchronous AADL language for modeling synchronous real-time systems in AADL, and provide a formal semantics for Synchronous AADL in Real-Time Maude. We have integrated into the OSATE modeling environment for AADL a plug-in which allows us to model check Synchronous AADL models in Real-Time Maude within OSATE. We exemplify such verification on an avionics system, whose Synchronous AADL design can be model checked in less than 10 seconds, but whose asynchronous design cannot be feasibly model checked.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Proceedings
Pages651-667
Number of pages17
DOIs
StatePublished - Nov 9 2011
Event13th International Conference on Formal Engineering Methods, ICFEM 2011 - Durham, United Kingdom
Duration: Oct 26 2011Oct 28 2011

Publication series

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

Other

Other13th International Conference on Formal Engineering Methods, ICFEM 2011
CountryUnited Kingdom
CityDurham
Period10/26/1110/28/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Synchronous AADL and its formal analysis in real-time maude'. Together they form a unique fingerprint.

Cite this