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

We have largely improved the model of the Fischer's mutual exclusion protocol, initially given in [BT03]. Our updated model can be found below.

Here you can download files with model and results of our check. It's available for IMITATOR and UPAALL
	UPPAAL	IMITATOR	Results	Unmodified IMITATOR results
1 state model	1StateSerializer.xml	Fischer1State.imi	Result1State.txt	UnmodifiedResult1State.txt
3 states model	3StatesSerializer.xml	Fischer3States.imi	Result3States.txt	UnmodifiedResult3States.txt

GREEN: One of the constraints.
RED:: 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.
BLUE:: 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.
YELLOW:: constraint is checked by three valuations.

[AK20]: É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]🌐
[BT03]: Roberto Barbuti, Luca Tesei: A Decidable Notion of Timed Non-Interference. Fundamenta Informaticae 54(2-3): 137-150 (2003)

Page made by Aleksander Kryukov.