Artifact instructions for “Efficient Verification of Lingua Franca Programs”

The code archive contains the source files and Docker configurations required to reproduce the results of our paper submission “Efficient Verification of Lingua Franca Programs”.

Below are instructions on how to set up the environment and run the experiments in Docker, followed by a description of the of the sources’ folder structure.

Docker Environment

In order to ensure a consistent environment for running the experiments, we provide ready-built Docker images for testing. You can pull and run the pre-built images from Github Container Registry.

This requires the reviewer to have Docker installed on their machine. Docker desktop is recommended for Windows and MacOS users. Linux users can follow the installation instructions for their specific distribution (instructions for Ubuntu can be found here).

To test lf-mc (contains both lf-maude and lf-mc) open a new shell session inside the docker instance (will download the image the first time the command is run, then reuse the cached image on subsequent runs):

The experiments are located in /opt/lf-maude/examples/src/ inside the docker instance. To compile and verify the TrainDoor_v3.lf example, run the following command:

We also provide native maude files that can be run with the following command inside Docker:

To test our real-time maude analysis, a separate Docker image is provided:

To run the analysis commands for the ADAS example, use the following command:

Source code Structure

Each subfolder within the archive contains the source files of its associated project.

code.zip/
├── lf-maude/
├── lf-mc/
└── lf-rt-maude/
checksum.txt

lf-maude

lf-maude contains the maude intepreter for lingua-franca.

lf-maude
├── absDynamics.maude
├── lf-main-concrete.maude
├── ...
└── examples
    ├── mod-gen
    │   ├── ADASModel
    │   │   └── ADASModel.maude
    │  ...
    │   └── UnsafeSend
    │       └── UnsafeSend.maude

    └── src
        ├── ADASModel.lf
       ...
        └── UnsafeSend.lf

At the root of the directory are the .maude files that implement our LF interpreter. The examples subfolder contains the case studies used in the experiments. The .maude files within are hand-written translation of the verification done in LF-verifier, together with additional analysis in some cases.
Inside examples/src/ are .lf files of LF-verifier together with annotations for analysis and physical actions. These are the files lf-mc reads to automatically generate the .maude files in examples/mod-gen/.

lf-mc

lf-mc contains the lingua franca compiler that automatically translates
.lf files with analysis annotations into maude files that can be run
by lf-maude.

lf-mc/
├ ...
├── core
│   └── src
│      ...
│       ├── main
│       │   ├── antlr
│       │   │   ├── LTLLexer.g4
│       │   │   ├── LTLParser.g4
│       │   │  ...
│       │   ├── java
│       │   │   └── org
│       │   │       └── lflang
│       │   │           ├── analyses
│       │   │           │   ├── c
│       │   │           │   │   ├── CToMaudeVisitor.java
│       │   │           │   │  ...
│       │   │           │   ├── maude
│       │   │           │   │   ├── LTLVisitor.java
│       │   │           │   │   ├── MaudeGenerator.java
│       │   │           │   │  ...
... # other files ommitted for brevity

This is a Java project built using gradle. The build used for this submission is included in the docker image referenced above, but also available here (requires java 1.7 to run). In order to build the project from source run the ./gradlew assemble command at the root of the lf-mc folder.

lf-rt-maude

lf-rt-maude contains the real-time analysis support for lingua-franca programs. This requires maude 2.7 to run, which conflicts with newer versions of maude and is the reason a separate Docker image has been provided.

lf-rt-maude
├── alarm.maude
├── pingPong.maude
├── RTM-ADAS.maude
├── rtm-aircraft-door.maude
├─ ...
├── thermostat.maude
└── TrainDoor_v3.maude

The .maude files shown above contain analysis done using timed CTL model checking.