# OSATE Slicer Supporting Archive

This archive contains a number of files supporting the paper (currently in submission to ECFMA22) "The OSATE Slicer: Graph-Based Reachability for Architectural Models"

## Overview

The included files and directories are:

1. aadl-projects: The AADL models used in the evaluation. See full description below in the "AADL Projects" section
2. awas-perf-out.txt: The complete, raw OSATE output generated when running the awas performance evaluation suite.
3. AwasMethods.java: A modification of an [existing project](https://github.com/osate/experimental/blob/master/isse/org.osate.isse.verificationmethods/src/org/osate/isse/verificationmethods/AwasMethods.java) used to execute Awas via the OSATE test infrastructure.
4. CMU-SEI-License.txt: The license for elements of this work created by CMU-SEI.
5. graphviz: Human-readable reachability graphs for each model, as generated by Awas and the OSATE Slicer.
6. licenses: License files governing the use / distribution of the models contained in the archive.
7. Performance Data.xlsx: The runtimes (collected from the two *-perf-out.txt files) and some basic calculations used to inform / support the manuscript's text.
8. README.md: This file
9. slicer-perf-out.txt: The complete, raw OSATE output generated when running the OSATE Slicer performance evaluation suite.
10. src: The code used to execute the performance evaluation, built on top of the [OSATE Test](https://github.com/osate/osate2/tree/master/core/org.osate.testsupport) infrastructure.

## AADL Projects

In publications describing Awas ([1],[2]), Thiagarajan et al evaluate their software on 11 open-source models. However, the models are distributed across several git repositories (which are controlled by different organizations), there are multiple versions of some of them, and many have multiple system implementations, so it's unclear which to instantiate / analyze. After corresponding with Thiagarajan, we have archived a copy of the models here to aid reproducibility, specified the exact implementation to instantiate (where known), and described modifications necessary for the Slicer and Awas to operate on the model (if any). Note also the license details, which apply to the various models.

1. Aircraft System
    * [aircraft-system/AircraftSystem.aadl "AircraftSystem.SubsystemImpl" (Line 49](https://github.com/osate/examples/blob/master/core-examples/aircraft-example/AircraftSystem.aadl#L49)
    * No modifications required
    * We were not informed which implementation was instantiated for the Awas evaluation, this is our best guess.
2. Display Manager
    * [display-manager/initial-model/integration.aadl "display_manager.i" (Line 19)](https://github.com/osate/examples/blob/e9564d21fa44c8b40a6ee11390fe59b5b5aad630/display-manager/initial-model/integration.aadl#L19)
    * One modification to fix an error:
        1. Change `arinc653::memory_type => (data_memory);` to `ARINC653::Memory_Kind => (Memory_Data);` in platform.aadl (Line 44)
3. Flight Guidance System
    * [SafetyTutorial/packages/FlightSystem.aadl "FlightSystem.tier1" (Line 82)](https://github.com/osate/examples/blob/e9564d21fa44c8b40a6ee11390fe59b5b5aad630/SafetyTutorial/packages/FlightSystem.aadl#L82)
    * Three modifications required to run (same model as #4):
        1. Add [s1|s2]toloc[So|Lpd|Id] in GPSParts.aadl (Lines 199-204)
        2. Split valueflow1 into two paths in AutomatedFlightGuidance.aadl (Lines 29-30)
        3. Add GPSPath[2|3] in AutomatedFlightGuidance.aadl (Lines 128-129)
    * Thiagarajan indicated that he tested the "FlightSystem.tier1parts" system implementation, but this is likely an error -- we have used FlightSystem.tier1 which extends tier1parts.
4. Flight Guidance Two GPS
    * [SafetyTutorial/packages/FlightSystem.aadl "FlightSystem.DualGPS" (Line 124)](https://github.com/osate/examples/blob/e9564d21fa44c8b40a6ee11390fe59b5b5aad630/SafetyTutorial/packages/FlightSystem.aadl#L124)
    * Three modifications required to run (same model as #3):
        1. Add [s1|s2]toloc[So|Lpd|Id] in GPSParts.aadl (Lines 199-204)
        2. Split valueflow1 into two paths in AutomatedFlightGuidance.aadl (Lines 29-30)
        3. Add GPSPath[2|3] in AutomatedFlightGuidance.aadl (Lines 128-129)
5. Isolette
    * [isolette-module/aadl/aadl/packages/Isolette.aadl "thermostat_single_sensor.impl" (Line 171)](https://github.com/santoslab/isolette-module/blob/41285fc3fcacd6094da35b76539d12a9a87cb489/aadl/aadl/packages/Isolette.aadl#L171)
    * No modifications required.
6. Open PCA Pump
    * [aadl-examples/awas-examples/open-pca/Functional_PCA/packages/iPCA_Medical_Device.aadl "PCA_Pump_System.i extends Platform::Generic_System.i" (Line 71)](https://github.com/santoslab/aadl-examples/blob/a82f01e003d6bb74f42e9682274b488c8e0725a2/awas-examples/open-pca/Functional_PCA/packages/iPCA_Medical_Device.aadl#L71)
    * We were unable to get this model to parse, and have not included it in the archive or evaluation.
7. Communication Router
    * This model could not be retrieved.
8. Speed Regulation
    * [speed-regulation/model/integration.aadl "integration.generic" (Line 22)](https://github.com/osate/examples/blob/e9564d21fa44c8b40a6ee11390fe59b5b5aad630/speed-regulation/model/integration.aadl#L22)
    * Three modifications to fix errors:
        1. Change `cmd: in data port speed_regulation::icd::speed_command.i;` to `cmd: in data port speed_regulation::icd::speed_command;` on line 296
        2. Same change, line 331
        3. Change the error library's name from `speed_regulation::error_library` to `speed_regulation_error_library` -- Awas's query parser doesn't seem to tolerate `:` characters
9. Simple UAV
    * [aadl-examples/awas-examples/CASE_simple_example/AADL/UAS.aadl "UAS.Impl" (Line 13)](https://github.com/santoslab/aadl-examples/blob/a82f01e003d6bb74f42e9682274b488c8e0725a2/awas-examples/CASE_simple_example/AADL/UAS.aadl#L13)
    * One modification to fix an error:
        * The `TB_SYS` property set referred to in MC.aadl doesn't exist, so I commented it out (line 12) and the properties used from it (lines 87-90).
10. AFRL UxAS
    * [OpenUxAS-SoI/AADL_project/aadl/models/UxAS.aadl "uxas.i" (Line 94)](https://github.com/afrl-rq/OpenUxAS-SoI/blob/81c7ad024a9d1bce0436ad2f4ca5742dda1a87a5/AADL_project/aadl/models/UxAS.aadl#L94)
    * No modifications required.
11. Wheel Brake System
    * [ARP4761/advanced/implementation/wbs.aadl "wbs.detailed" (Line 98)](https://github.com/osate/examples/blob/e9564d21fa44c8b40a6ee11390fe59b5b5aad630/ARP4761/advanced/implementation/wbs.aadl#L98)
    * Two modifications to enable graph construction:
        1. Added output types to a number of error paths in `valves.aadl` (both in simple and implementation folders, since it seems that there's some cross-linking between the two?)
        2. Renumbered error paths in the `command_shutoff` system in both `valves.aadl` files. The first path was named `f1`, which is the same name as the path in the generic type, which is extended. That overwrote the original path, which then crashed when tokens tried to get propagated into it. 
12. Wheel Brake System -- Large
    * [WBS_arch4_v3/packages/WBS.aadl "WBS.inst" (Line 79)](https://github.com/loonwerks/AMASE/blob/master/examples/WBS_arch4_v3/packages/WBS.aadl#L79)
    * No modifications required.
    * Not part of the evaluation of the original 11 from Thiagarajan et al's publications.

### Licenses

1. Models from the santoslab repository: Licensed under BSD-2, see https://github.com/sireum/v3/blob/master/license.txt or the KSU-BSD-2.txt file in the licenses directory.
2. Models from the afrl-rq repository: Licensed under the USAF Open Source Agreement, see https://github.com/afrl-rq/OpenUxAS-SoI/blob/81c7ad024a9d1bce0436ad2f4ca5742dda1a87a5/LICENSE.md or the AFRL-USAF-OSA.md file in the licenses directory.
3. Models from the loonwerks repository: Licensed under BSD-3, see https://github.com/loonwerks/AMASE/blob/master/LICENSE or the Collins-BSD-3.txt file in the licenses directory.
4. Models from the osate repository: See CMU-SEI-License.txt in the licenses directory.

## Running the evaluation

The evaluation from the paper can be recreated using the `org.osate.slicer.evaluation` and `org.osate.awas.evaluation` packages, which are JUnit test suites. They require the OSATE test infrastructure, see https://osate.org for instructions on setting up an OSATE development environment, or reach out to the author (Sam Procter sprocter@sei.cmu.edu) for assistance. Running the Awas evaluation requires Awas, see https://awas.sireum.org/ for installation instructions.

[1]: https://doi.org/10.1007/978-3-030-59155-7_23
[2]: https://doi.org/10.1007/s11334-021-00410-w

