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
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.
The version of IMITATOR used to solve the challenges is IMITATOR 2.7-beta2 (build 1073).
- 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
./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)
- É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]
- 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)]