A number of 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 verification is typically unfeasible due to the state space explosion caused by the interleavings. The Multirate PALS formal pattern reduces the problem of designing and model checking such 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 work 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.
The Multirate Synchronous AADL model of the airplane turning controller example from our paper is provided below. The archive file contains AADL source code (in packages directory) and the requirement specification (in verification directory).
We have also defined a model of the control algorithm directly in Real-Time Maude; the model is available for download here.
Two additional avionics examples for sintle-rate Synchronous AADL are also available here.
We define an executable formal semantic for Multirate Synchronous AADL. In addition to the Maude system, this semantic also requires the Real-Time Maude. We also give the Real-Time Maude models of the airplane turning controller that are automatically generated from the Multirate Synchronous AADL model by the MR-SynchAADL tool.
This semantics is significantly adapted from the generic Real-Time Maude framework for specifying Multirate PALS models, available here.
MR-SynchAADL is an Eclipse plug-in to model check Multirate Synchronous AADL models in the OSATE environment. Our tool requires the following tools and plug-ins:
For the sake of convenience, we also provide the zip file that contains the plugins for both Maude development tools and MR-SynchAADL.
After install all the tools and plugins, you can test our case study by importing the entire AirplaneTurn directory as a project by choosing File/Import/General/Existing Projects into Workspace in the menu. The MR-SynchAADL view can be seen by choosing Window/Show View/Other/SynchAADL/SynchAADL Verifier in the menu.
An older version of our tool for single-rate Synchronous AADL, as well as two avionics examples, are available to download here.
The following manuscript gives more details about Multirate Synchronous AADL, its Real-Time Maude semantics, and the airplane case study.
Multirate Synchronous AADL and the MR-SynchAADL tool (including old versions for single-rate PALS) are explained in:
The theoretical foundations of the Multirate PALS methodology are presented in:
A Real-Time Maude model of the airplane case study and its analysis using Multirate PALS are illustrated at: