CAV 2021

This page explains the artifact for our paper: "HYBRIDSYNCHAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL" by J. Lee, S. Kim, K. Bae, and P. C. Ölveczky. The artifact includes the HybridSynchAADL tool and the scripts for running the experiments in the paper.

A VirtualBox image for the artifact is available at http://doi.org/10.5281/zenodo.4699760. In the virtual machine, the artifact is located in the directory home/user/CAV2021-AeC. See Readme.txt in the directory for more details about the tool and experiments.

Running the Artifact in a non-VM Environment

We explain how to install and run the artifact in a non-VM environment. The artifact requires the following libraries:

• JAVA 8: https://openjdk.java.net/install/
• GNU parallel: https://www.gnu.org/software/parallel/

To install our artifact, download and unzip the following archive file which contains the benchmark models and scripts in the directory CAV2021-AeC:

artifact.zip

The archive file already contains the following tools. Maude-SE is needed for the HybridSynchAADL tool, and the other tools are used for the experiments.

• Maude-SE: https://maude-se.github.io/
• SpaceEx: http://spaceex.imag.fr/
• Flow*: https://flowstar.org/
• HyComp: https://es-static.fbk.eu/tools/hycomp/
• dReach: http://dreal.github.io/

For Ubuntu, we provide a script (set-up.sh) to install Java 8 and GNU parallel, if not already installed.

The above instructions also apply when creating a new VM image. For example, you can create a new VirtualBox image with Ubuntu installed, unzip artifact.zip on the virtual machine, and run set-up.sh in the directory CAV2021-AeC to install the required libraries for the artifact.

Setting up the HybridSynchAADL Tool

In the artifact, the HybridSynchAADL tool is located in the directory CAV2021-AeC/hybridsynchaadl/osate. For the workspace, use the directory CAV2021-AeC/hybridsynchaadl/workspace, which includes a HybridSynchAADL model FourDronesSystem. 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.