ISOLA 2022

This page explains the artifact for our paper: "An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs" by J. Lee, K. Bae, and P. C. Ölveczky. This page includes the HybridSynchAADL tool, case study model, and executable formal semantics.

Complete AADL Specification for the Case Study

The 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 HybridSynchAADL

We also defines an executable formal semantic for this case study. This semantics is significantly adapted from this paper and extended to deal with array data types, arrays of components and ports, and subprograms.

• semantics.zip

The HybridSynchAADL Tool

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

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

In the artifact, HybridSynchAADL tool can be exeucted by double clicking /hybridsynchaadl/osate. For the workspace, use the directory /hybridsynchaadl/workspace, which includes a 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.