IMITATOR: Experiments Data for TASE 2019

Case Studies Related to "Formalizing Time4sys using parametric timed automata"

Paper: Formalizing Time4sys using parametric timed automata [Andre19].

The version of IMITATOR used to run the experiments is IMITATOR v2.10.4.

Source code from GitHub
Binary (Ubuntu-like, Debian-like 64 bits); this binary is standalone and can hence be executed without any external library

Non-parametric schedulability analysis: model result log
Parametric WCETs for tasks 1 and 4: model result log cartography (2D)
Parametric WCETs for tasks 1, 4, 5 and 7: model result log cartography (2D)
Parametric deadlines for tasks 1 and 5: model result log cartography (2D)
Parametric offset for task 1: model result log
Parametric deadlines and WCETS for tasks 1 and 5 : model result log cartography (2D)
Parametric offset, WCET and deadline for task 1: model result log cartography (2D)

We conducted the experiments on a Dell XPS 13 9365 i7 (2017) running Linux Mint 18.2 64 bits with 8 GiB memory.

For all case studies, the following command was used for PTPM:

> ./imitator [case_study.imi] -mode EF -incl -merge -output-result -output-cart

[Andre19]: Étienne André. Formalizing Time4sys using parametric timed automata. In Dominique Méry and Shengchao Qin (eds.), TASE’19, IEEE, pages 176–183, July 2019. DOI: 10.1109/TASE.2019.00031 (English) [PDF (author version) | BibTeX | Slides]🌐