Synchronous AADL and its Formal Analysis in Real-Time Maude

Bae, Kyungmin; Olveczky, Peter C.; Al-Nayeem, Abdullah; Meseguer, José

Permalink

https://hdl.handle.net/2142/25091 Copy

Description

Title

Synchronous AADL and its Formal Analysis in Real-Time Maude

Author(s)

• Bae, Kyungmin
• Olveczky, Peter C.
• Al-Nayeem, Abdullah
• Meseguer, José

Issue Date

2011-05-31

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/25091

Sponsor(s)/Grant Number(s)

• Boeing/C8088
• CNS 08-34709
• CCF 09-05584
• The Research Council of Norway

Owning Collections