The IMITATOR benchmarks library (v1.0)

• Home
• Download
• Benchmarks
• Publications
• FAQ
• Contact
• Links

The IMITATOR benchmarks library (v1.0)

This page presents the official IMITATOR benchmarks library in its first version [Andre18]. These models have been accumulated over the years from scientific publications, and from industrial collaborations.

This version of the library contains 34 benchmarks with 80 different models and 122 properties.

The models are all compatible with IMITATOR v.2.12 Butter Lobster.

For robustness analysis, the reference valuation can be obtained in the IM column.

Benchmark	Source	Categories										Metrics									Property
		Academic	Automotive	Educ.	Hardw.	Industrial	ProdCons	Protocol	RTS	Sched	Toy	|PTA|	|X|	|P|	|D|	|L|	|Act|	L/U?	Inv?	SW?	Reach.	Safety	Pattern	Opt.	IM
And-Or	[CC05]	yes	no	no	yes	no	no	no	no	no	no	4	4	12	0	27	8	L/U-PTA	yes	no	no	no	yes	no	no
Bounded retransmission protocol	[DKRT97]	yes	no	no	no	yes	no	yes	yes	no	no	6	7	2	12	22	12	Not L/U	yes	no	no	yes	no	no	no
Not-Not-And circuit	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	6	0	8	20	L/U-PTA	yes	no	no	yes	no	no	no
Not-Not-And circuit	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	6	0	8	20	L/U-PTA	yes	no	no	no	no	no	yes
3NotAnd	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	10	0	22	9	L/U-PTA	yes	no	no	yes	no	no	no
3NotAnd	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	10	0	22	9	L/U-PTA	yes	no	no	no	no	no	yes
3NotAnd	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	10	0	22	9	L/U-PTA	yes	no	no	no	no	no	yes
coffee machine		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	4	4	Not L/U	yes	no	yes	no	no	no	no
coffee machine		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	4	4	Not L/U	yes	no	no	no	no	no	no
coffee machine		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	4	4	Not L/U	yes	no	no	no	no	no	yes
Coffee machine + drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	yes	no	no	no
Coffee machine + drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	no	no	no	yes
Coffee machine + unbounded drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	yes	no	no	no
Coffee machine + unbounded drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	no	no	no	yes
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	19	9	Not L/U	yes	no	yes	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	19	9	Not L/U	yes	no	no	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	19	9	Not L/U	yes	no	no	no	no	no	yes
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	525	9	Not L/U	yes	no	yes	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	525	9	Not L/U	yes	no	no	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	525	9	Not L/U	yes	no	no	no	no	no	yes
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	4115	9	Not L/U	yes	no	yes	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	4115	9	Not L/U	yes	no	no	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	4115	9	Not L/U	yes	no	no	no	no	no	yes
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	8213	9	Not L/U	yes	no	yes	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	8213	9	Not L/U	yes	no	no	no	no	no	no
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	8213	9	Not L/U	yes	no	no	no	no	no	yes
Fischer (L/U-PTA)	[AHV93]	yes	no	no	no	no	no	yes	yes	no	no	3	2	4	0	10	10	L/U-PTA	no	no	no	yes	no	no	no
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	2	2	4	1	8	0	L/U-PTA	yes	no	no	yes	no	no	no
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	2	2	4	1	8	0	L/U-PTA	yes	no	no	no	no	no	yes
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	3	3	4	1	12	0	L/U-PTA	yes	no	no	yes	no	no	no
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	3	3	4	1	12	0	L/U-PTA	yes	no	no	no	no	no	yes
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	2	2	2	2	10	12	L/U-PTA	yes	no	no	yes	no	no	no
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	2	2	2	2	10	12	L/U-PTA	yes	no	no	no	no	no	yes
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	3	3	2	2	15	18	L/U-PTA	yes	no	no	yes	no	no	no
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	3	3	2	2	15	18	L/U-PTA	yes	no	no	no	no	no	yes
Fischer (unknown origin)		yes	no	no	no	no	no	yes	yes	no	no	3	2	2	1	9	11	L/U-PTA	yes	no	no	yes	no	no	no
Fischer (unknown origin)		yes	no	no	no	no	no	yes	yes	no	no	3	2	2	1	9	11	L/U-PTA	yes	no	no	no	no	no	yes
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	4	2	2	1	13	8	L/U-PTA	no	no	no	yes	no	no	no
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	4	2	2	1	13	8	L/U-PTA	no	no	no	no	no	no	yes
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	5	3	2	1	18	12	L/U-PTA	no	no	no	yes	no	no	no
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	5	3	2	1	18	12	L/U-PTA	no	no	no	no	no	no	yes
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	6	4	2	1	23	16	L/U-PTA	no	no	no	yes	no	no	no
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	6	4	2	1	23	16	L/U-PTA	no	no	no	no	no	no	yes
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	7	5	2	1	28	20	L/U-PTA	no	no	no	yes	no	no	no
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	7	5	2	1	28	20	L/U-PTA	no	no	no	no	no	no	yes
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	12	10	2	1	53	40	L/U-PTA	no	no	no	yes	no	no	no
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	12	10	2	1	53	40	L/U-PTA	no	no	no	no	no	no	yes
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	2	0	52	12	U-PTA	yes	no	no	yes	no	no	no
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	2	0	52	12	U-PTA	yes	no	no	no	no	no	yes
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	4	0	52	12	U-PTA	yes	no	no	yes	no	no	no
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	4	0	52	12	U-PTA	yes	no	no	no	no	no	yes
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	12	0	52	12	U-PTA	yes	no	no	yes	no	no	no
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	12	0	52	12	U-PTA	yes	no	no	no	no	no	yes
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	2	8	4	18	4	Not L/U	yes	no	yes	no	no	yes	no
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	2	8	4	18	4	Not L/U	yes	no	no	no	no	no	yes
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	3	12	4	27	3	Not L/U	yes	no	yes	no	no	yes	no
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	3	12	4	27	3	Not L/U	yes	no	no	no	no	no	yes
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	4	4	16	4	36	4	Not L/U	yes	no	yes	no	no	yes	no
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	4	4	16	4	36	4	Not L/U	yes	no	no	no	no	no	yes
Cooking noodles		no	no	yes	no	no	no	no	no	no	yes	1	2	2	0	4	4	Not L/U	yes	no	no	yes	no	no	no
Nuclear plant		no	no	yes	no	no	no	no	no	no	yes	1	2	4	0	6	6	Not L/U	yes	no	no	yes	no	no	no
Packaging		yes	no	no	no	no	yes	no	no	no	no	3	2	2	0	10	6	L/U-PTA	yes	no	yes	no	no	no	no
Packaging		yes	no	no	no	no	yes	no	no	no	no	3	2	2	0	10	6	L/U-PTA	yes	no	no	no	no	no	yes
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	5	5	6	0	16	11	L/U-PTA	yes	no	yes	no	no	no	no
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	5	5	6	0	20	15	L/U-PTA	yes	no	yes	no	no	no	no
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	6	6	6	0	18	12	L/U-PTA	yes	no	yes	no	no	no	no
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	6	6	6	0	21	15	L/U-PTA	yes	no	yes	no	no	no	no
Root contention protocol	[CS01]	no	no	no	no	yes	no	yes	yes	no	no	5	6	5	6	48	16	L/U-PTA	yes	no	yes	no	no	no	no
Root contention protocol	[CS01]	no	no	no	no	yes	no	yes	yes	no	no	5	6	5	6	48	16	L/U-PTA	yes	no	no	no	no	no	no
Root contention protocol	[CS01]	no	no	no	no	yes	no	yes	yes	no	no	5	6	5	6	48	16	L/U-PTA	yes	no	no	no	no	no	no
SSLAF14 test 1	[SSLAF13]	no	no	no	no	no	no	yes	yes	no	no	7	16	2	2	42	23	Not L/U	yes	yes	no	yes	no	no	no
SSLAF14 test 2	[SSLAF13]	no	no	no	no	no	no	yes	yes	no	no	6	14	2	4	45	26	Not L/U	yes	yes	no	yes	no	no	no
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	Not L/U	yes	no	no	yes	no	no	no
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no
SLAF14	[SLAF14]	yes	no	no	no	no	no	yes	yes	no	no	8	13	2	3	47	17	Not L/U	yes	yes	no	yes	no	no	no
SLAF14	[SLAF14]	yes	no	no	no	no	no	yes	yes	no	no	12	21	2	0	153	29	Not L/U	yes	yes	no	yes	no	no	no
FMTV Challenge 1A	[SAL15]	no	no	no	no	yes	no	yes	yes	no	no	3	3	3	5	15	9	Not L/U	yes	no	yes	no	no	yes	no
FMTV Challenge 1A	[SAL15]	no	no	no	no	yes	no	yes	yes	no	no	3	3	3	7	15	12	Not L/U	yes	no	yes	no	no	yes	no
FMTV Challenge 2	[SAL15]	no	no	no	no	yes	no	yes	yes	no	no	6	9	2	0	87	21	Not L/U	yes	yes	yes	no	no	yes	no
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	2	0	46	16	Not L/U	yes	no	yes	no	no	no	no
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	2	0	46	16	Not L/U	yes	no	no	no	no	no	yes
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	3	0	46	16	Not L/U	yes	no	yes	no	no	no	no
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	3	0	46	16	Not L/U	yes	no	no	no	no	no	yes
train1PTA		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	5	4	Not L/U	yes	no	no	yes	no	no	no
train1PTA		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	5	4	Not L/U	yes	no	no	no	no	no	yes
TrainAHV93	[AHV93]	yes	no	no	no	no	no	no	no	no	no	3	3	6	0	12	8	L/U-PTA	no	no	no	yes	no	no	no
TrainAHV93	[AHV93]	yes	no	no	no	no	no	no	no	no	no	3	3	6	0	12	8	L/U-PTA	no	no	no	yes	no	no	no
SPSMALL	[CEFX09][Andre10]	no	no	no	yes	yes	no	no	no	no	no	11	11	2	0	52	25	Not L/U	yes	no	yes	no	no	no	no
SPSMALL	[CEFX09][Andre10]	no	no	no	yes	yes	no	no	no	no	no	11	11	2	0	52	25	Not L/U	yes	no	no	no	no	no	yes
SPSMALL	[CEFX09][Andre10]	no	no	no	yes	yes	no	no	no	no	no	11	11	26	0	52	25	Not L/U	yes	no	yes	no	no	no	no
SPSMALL	[CEFX09][Andre10]	no	no	no	yes	yes	no	no	no	no	no	11	11	26	0	52	25	Not L/U	yes	no	no	no	no	no	yes
WFAS	[BBLS15]	yes	no	no	no	no	no	no	no	no	no	3	4	2	0	10	4	Not L/U	yes	no	no	yes	no	no	no
WFAS	[BBLS15]	yes	no	no	no	no	no	no	no	no	no	3	4	2	0	10	4	Not L/U	yes	no	no	no	no	no	yes
WFAS	[BBLS15]	yes	no	no	no	no	no	no	no	no	no	3	4	2	0	10	4	Not L/U	yes	no	no	no	no	no	yes
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	2574	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	4909	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	7814	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	10060	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	12546	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	15390	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	17703	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	20314	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	22706	10	Not L/U	yes	no	yes	no	no	no	no
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	25152	10	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	1475	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	2845	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	4603	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	5847	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	7309	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	9003	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	10323	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	11839	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	13191	6	Not L/U	yes	no	yes	no	no	no	no
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	14665	6	Not L/U	yes	no	yes	no	no	no	no
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	208	4	Not L/U	yes	no	yes	no	no	no	no
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	408	4	Not L/U	yes	no	yes	no	no	no	no
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	608	4	Not L/U	yes	no	yes	no	no	no	no
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	808	4	Not L/U	yes	no	yes	no	no	no	no
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	1008	4	Not L/U	yes	no	yes	no	no	no	no

References

[ACDFR09]

Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Silvain Ruel. Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In Didier Lime and Olivier H. Roux (eds.), MSR’09, Journal Européen des Systèmes Automatisés 43(7-9), Hermès, pages 1049–1064, 2009.

[ACR16]

Étienne André, Thomas Chatain and César Rodríguez. Preserving Partial Order Runs in Parametric Time Petri Nets. Transactions on Embedded Computing Systems 16(2), pages 43:1–43:26, December 2016. (English) [PDF | BibTeX]

[AHV93]

Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.

[AHW18]

Étienne André, Ichiro Hasuo and Masaki Waga (和賀 正樹). Offline timed pattern matching under uncertainty. In Anthony Widjaja Lin and Jun Sun (eds.), ICECCS’18, IEEE CPS, pages 10–10, December 2018. (English) [BibTeX | Slides]

[Andre10]

Étienne André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010.

[Andre18]

Étienne André. A benchmarks library for parametric timed model checking. In Cyrille Artho and Peter Csaba Ölveczky (eds.), FTSCS’18, Springer CCIS 1008, pages 75–83, November 2018. Acceptance rate: 45%. DOI: 10.1007/978-3-030-12988-0_5 (English) [PDF (author version) | BibTeX | data | Slides]🌐

[BBLS15]

Nikola Beneš, Peter Bezděk, Kim Guldstrand Larsen, Jirí Srba: Language Emptiness of Continuous-Time Parametric Timed Automata. In ICALP 2015, Part II, volume 9135 of LNCS, pages 69-81. Springer, 2015.

[CC05]

Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.

[CC07]

Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In Science of Computer Programming 64(1), pages 115-139, 2007.

[CEFX09]

Rémy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, and Weiwen Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, 2009.

[CS01]

Aurore Collomb-Annichini and Mihaela Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In Proceedings of the Real-Time Tools Workshop (RT-TOOLS’2001).

[DKRT97]

Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans: The Bounded Retransmission Protocol Must Be on Time! TACAS 1997: 416-431.

[HAF14]

Bardh Hoxha, Houssam Abbas, Georgios E. Fainekos: Benchmarks for Temporal Logic Requirements for Automotive Systems. ARCH@CPSWeek 2014: 25-30

[HRSV02]

Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52-53: 183-220 (2002)

[JLR13]

Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 401–415. Springer, 2013.

[KNSW07]

Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, and Fuzhi Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007.

[KP12]

Michał Knapik, Wojciech Penczek: Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets and Other Models of Concurrency 5: 141-159 (2012)

[PS08]

Wojciech Penczek, Maciej Szreter. SAT-based Unbounded Model Checking of Timed Automata. Fundam. Inform. 85(1-4): 425-440 (2008)

[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)]

[SLAF14]

Giuseppe Lipari, Sun Youcheng (孙有程), Étienne André and Laurent Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In Étienne André and Goran Frehse (eds.), SynCoP’14, EPTCS 145, pages 49–64, April 2014. (English) [PDF | BibTeX]

[SSLAF13]

Sun Youcheng, Romain Soulat, Giuseppe Lipari, Étienne André and Laurent Fribourg. Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems. In Cyrille Artho and Peter Ölveczky (eds.), FTSCS’13, Volume 419 of Communications in Computer and Information Science, Springer, pages 212–228, October 2013. (English) [PDF (author version) | Slides]