IMITATOR: Experiments Data for ICECCS 2020
Case Studies Related to "Parametric non-interference in timed automata"
Paper: Parametric non-interference in timed automata [AK20].
The version of IMITATOR used to run the experiments was presumably IMITATOR v2.12 "Butter Lobster".
- Source code from GitHub
- Binary (Ubuntu-like, Debian-like 64 bits); this binary is standalone and can hence be executed without any external library
New version of the Fischer's mutual exclusion protocol
We have largely improved the model of the Fischer's mutual exclusion protocol, initially given in [BT03]. Our updated model can be found below.
Description of results
- One of the constraints.
- this number means that IMITATOR gave this constraint for both models. A number for one constraint is the same in both files. Valuations for these constraints are written only in results of 1 state model.
- constraint is checked by only one valuation if acc > ucs because even if both processors will be in the state iWantAccess_1/2 and one of them will enter the CS state, for example the 1st, it will exit CS state before the 2nd can enter it because of “acc” time units.
- constraint is checked by three valuations.
- Étienne André and Aleksander Kryukov. Parametric non-interference in timed automata. In Yi Li and Alan Liew (eds.), ICECCS’20, October 2020. To appear. (English) [PDF (author version) | data]🌐
- Roberto Barbuti, Luca Tesei:
A Decidable Notion of Timed Non-Interference. Fundamenta Informaticae 54(2-3): 137-150 (2003)
Page made by Aleksander Kryukov.