Files in this item



application/pdfs-a-techrep.pdf (680kB)
(no description provided)PDF


Title:Synchronous AADL and its Formal Analysis in Real-Time Maude
Author(s):Bae, Kyungmin; Olveczky, Peter C.; Al-Nayeem, Abdullah; Meseguer, José
Subject(s):Architecture Analysis & Design Language (AADL)
model checking
formal verification
Real-Time Maude
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 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.
Issue Date:2011-05-31
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
CNS 08-34709
CCF 09-05584
The Research Council of Norway
Date Available in IDEALS:2011-05-31

This item appears in the following Collection(s)

Item Statistics