IMITATOR: Experiments Data for FMTV 2015

Thales’ Formal Methods for Timing Verification Challenge (FMTV 2015)

This page is dedicated to the case studies related to the manuscript Verification of Two Real-Time Systems Using Parametric Timed Automata by Sun Youcheng, Étienne André and Giuseppe Lipari, presented at WATERS’15 [SAL15].

The Thales Challenge

The challenge was presented at the FMTV workshop in Singapore. The challenge was then formalized in a PDF document. The solutions were presented at WATERS’15 in Lund, Sweden.

IMITATOR

The version of IMITATOR used to solve the challenges is IMITATOR 2.7-beta2 (build 1073).

Download

Source code
Standalone binary (Ubuntu-like, Debian-like 64 bits); compiled without the distributed capabilities of IMITATOR (not used here anyway)

Models for challenge 1A

fmtv1A1-v2.imi (model for n=1) [graphics]
fmtv1A3-v2.imi (model for n=3) [graphics]
parseIMI.py (post-processing Python script)

Commands

./imitator fmtv1A1-v2.imi -mode EF -output-result -merge -incl && python parseIMI.py fmtv1A1-v2.res

Expected result: e2e in [63.0,145.008]

./imitator fmtv1A3-v2.imi -mode EF -output-result -merge -incl && python parseIMI.py fmtv1A3-v2.res

Expected result: e2e in [63.0,225.016]

Models for challenge 1B

Models for challenge 2

(not available as part of this artifact)

References

[ALS15]: Étienne André, Giuseppe Lipari and Sun Youcheng. IMITATOR: Formal Verification of Real-Time Systems Under Uncertainty. In Steve Goddard and Harini Ramaprasad (eds.), ECRTS’15 posters, July 2015. (English) [PDF]
[SAL15]: Sun Youcheng, Étienne André and Giuseppe Lipari. Verification of Two Real-Time Systems Using Parametric Timed Automata. In Sophie Quinton and Tullio Vardanega (eds.), WATERS’15, July 2015. (English) [PDF (author version)]

Contact

Étienne André