STTT 2021
This page explains the artifact for our paper: "Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL" by J. Lee, K. Bae, , P. C. Ölveczky, S. Kim, M, Kang. The artifact includes the HybridSynchAADL tool and the scripts for running the experiments in the paper. Apart from providing significantly more detail, this paper extends our conference tool paper.
Formal semantics for HybridSynchAADL
We define the formal semantics of HybridSynchAADL using Maude with SMT solving.
HybridSynchAADL components are symbolically represented as Maude terms with SMT
constraints. We thoroughly tested the formal semantics and the generated
models. We developed a test suite for unit testing of the equations and rules
in the formal semantics, and a test suite for system testing of the code
generation and state merging. The test suites are located in
semantics/test
Benchmark Models
In the paper, we analyzed HybridSynchAADL models: networked watertank, thermostat controllers, and rendezvous and formation control for distrubted drones. For other tools(SpaceEx, Flowstar, HyComp, and dReach), we encoded the synchronous designs of the HybridSynchAADL models as networks of hybrid automata.
HybridSynchAADL tool
To install our hybridsynchaadl tool, download and unzip the following archive files: tool.zip The artifact requires the following libraries:
- JAVA 11+: https://openjdk.java.net/install/
- Maude-SE: https://maude-se.github.io/
In the artifact, the HybridSynchAADL tool is located in the directory
hybridsynchaadl/osate. For the workspace, use the directory
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.
Artifact
We provide the artifact to reproduce the results in our paper. The artifact includes semantics, models, tools, scripts to automatically perform experiments and Readme.txt.