# Overview

Guide shows how to compile and run the accompanying material for the TECS submission titled "Worst-Case Execution Time Calculation for Query-Based Monitors by Witness Generation". This folder has two folders, relax and relax-analysis, while it has some other supplementary files.


# Getting Started and Requirements

Hardware:
* XMC4500 Relax Kit https://www.infineon.com/cms/en/product/evaluation-boards/kit_xmc45_relax_v1/

Software tools:
* Python3 https://www.python.org/downloads/
* PlatformIO https://pypi.org/project/platformio/
* OTAWA http://www.tracesgroup.net/otawa/download/64-2/ or obtain the Eclipse plugin and use the binary packaged with it http://www.tracesgroup.net/otawa/download/download-eclipse-plugin/ Important: we were NOT using the OTAWA V2.0 (which is still not released, but available for download)
* OTAWA script for Infineon XMC4500 microcontroller https://github.com/uastw-sat/ARMv7t-WCET-Analysis
* aiT timing analyzer for ARM


## Patching the initial OTAWA script

1. Clone the repository from https://github.com/uastw-sat/ARMv7t-WCET-Analysis locally (assumed that it is cloned under _~/git/_)
2. Apply the patch to the OTAWA script included in this package to turn off cache analysis feature
```
patch ~/git/ARMv7t-WCET-Analysis/XMC4500_OTAWA_Script_v2/xmc4500.osx < 0001-Remove-cache-analysis-from-OTAWA-XMC4500-script.patch
```


# Replicate execution time measurement results (RQ1)

The experiments are carried out on the XMC4500 microcontroller

The current version of Platformio does not have inbuilt support for the used Infineon Relax Lite Kit-V1, so the setup starts with adding support for this board:

1. Assuming the installation folder for PlatformIO _~/.platformio_, the file _~/.platformio/platforms/infineonxmc/builder/main.py_ needs to be patched with the patch included under _platformio-config_
```
patch ~/.platformio/platforms/infineonxmc/builder/main.py < 0002-Add-XMC4500-support.patch
```
2. Add the board description included in this package to the PlatformIO installation
```
cp xmc4500_relax_lite_kit.json /home/marci/.platformio/platforms/infineonxmc/boards
```

To run the measurements, follow the steps from the command line: 

1. Build the project in the _relax_ directory (`cd relax`) with `platformio run`.
2. Run the measurement campaign with `./measurements.sh`.
3. The results.csv will have 504 lines for each of the four queries:
 * the first 250 results are execution times over random models
 * the second 250 results are execution times over consistent models
 * the last 4 results are execution times over the generated witness models in the order of witness for close trains, witness for end of siding, witness for misaligned turnout, and witness for train locations (discard the 3 which do not belong to the repsective query)


# Execute WCET analysis 

1. Go to the _relax-analysis_ folder (`cd relax-analysis`) and edit the _src/main.c_ to include the query function and optionally a model. 
2. Build the project in the _relax-analysis_ with `platformio run`.
3a. To run the analysis with aiT, use the respective aiT files in the _relax-analysis/ait-resources_ to provide the analyzer flow facts. The different configuration modes of the analyzer are included in the paper.
3b. To run the analysis with OTAWA, use the example commands included in _relax-analysis/otawa-resources_ folder. After setting the loop bounds in the respective flow fact files, Otawa does not require further configuration.

