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".


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.

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

Description of results

Here should be an auxiliary picture
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.

Étienne André