IMITATOR

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

Models for challenge 1A

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. Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0) (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é