ISOLA 2024

This page explains the artifact for our paper: "Rigorous Model Engineering of Multirate CPSs in Multirate HybridSynchAADL" by J. Lee, K. Bae, and P. C. Ölveczky. This page includes the MR-HybridSynchAADL tool, case study model, and executable formal semantics.

Complete AADL Specification for the Case Study

The MR-HybridSynchAADL model of the packet delivery system example from out paper is provided below. The archive file contains AADL source code (in packages directory) and the requirement specification (in requirements directory).

• model.zip

Formal Semantics for MR-HybridSynchAADL

We also defines an executable formal semantic for this case study. This semantics is significantly adapted from this paper.

• semantics.zip

The MR-HybridSynchAADL Tool

To install our MR-HybridSynchAADL tool, download and unzip the following archive files: tool.zip The MR-HybridSynchAADL tool requires the following libraries:

• JAVA 11+: https://openjdk.java.net/install/
• Maude-SE: https://maude-se.github.io/

In the artifact, MR-HybridSynchAADL tool can be exeucted by double clicking /hybridsynchaadl/osate. For the workspace, use the directory /hybridsynchaadl/workspace, which includes a MR-HybridSynchAADL model PacketDeliverySystem. You also need to set the Maude path: in the top menu, go to Window => Preferences => Maude Preferences, and fill the Maude directory and executable Maude file.