Time4sys2imi: Experiments Data for ICTAC 2019

Time4sys2imi: A tool to formalize real-time system models under uncertainty

How to use?

How to install ?

Method 1: Installing Time4sys2imi for Linux

- Time4sys2imi tool : download jar file.
- Dependencies:
- IMITATOR:
The version of IMITATOR used to run the experiments is IMITATOR v2.10.4.
Download:
- Source code from GitHub.
- Binary (Ubuntu-like, Debian-like 64 bits); this binary is standalone and can hence be executed without any external library.
- Time4sys:
Link to download Time4sys.
Method 2: Installing Time4sys2imi for Windows/ Mac/ Linux

- Download (4.3 Go) virtual machine that contains time4sys2imi and its dependencies and run it using virtualbox.

Experiments:

Example1: This example contains 4 tasks without task chains executed in a single CPU
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep2: result
  - Parametric WCETStep2 and BCETStep2: result
  - Parametric WCETStep2, BCETStep2 and deadlineStep4: result
Example2: This example contains 3 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep1: result
  - Parametric WCETStep1 and BCETStep1: result
  - Parametric WCETStep1, BCETStep1 and deadlineStep1: result
Example3: This example contains 3 tasks executed in a single CPU.
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep3: result
  - Parametric WCETStep3 and BCETStep3: result
  - Parametric WCETStep3, BCETStep3 and deadlineStep3: result
Example4: This example contains 4 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep4: result
  - Parametric WCETStep4 and BCETStep4: result
  - Parametric WCETStep4, BCETStep4 and deadlineStep4: result
Example5: This example contains 3 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep3: result
  - Parametric WCETStep3 and BCETStep3: result
  - Parametric WCETStep3, BCETStep3 and deadlineStep3: result
Example6: This example contains 7 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep7: result
  - Parametric WCETStep7 and BCETStep7: result
  - Parametric WCETStep7, BCETStep7 and deadlineStep7: result
Example7: This example contains 4 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep3: result
  - Parametric WCETStep3 and BCETStep3: result
  - Parametric WCETStep3, BCETStep3 and deadlineStep3: result
Example8: This example contains 8 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep3: result
  - Parametric WCETStep3 and BCETStep3: result
  - Parametric WCETStep3, BCETStep3 and deadlineStep3: result
Example9: This example contains 11 tasks
- Model:
- Translation to PTAs:
- IMITATOR file: IMITATOR file
- Results:
  - Non-parametric: result
  - Parametric deadlineStep8: result
  - Parametric WCETStep8 and BCETStep8: result
  - Parametric WCETStep8, BCETStep8 and deadlineStep8: result

We conducted the experiments on a ASUS X411UN i7-8550U running Linux Mint 19 64bits with 8GiB memory.