Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets

Sine Lyhne Viesmose, Thomas Stig Jacobsen, Jacob Jon Jensen, Christoffer Moesgaard, Niels Nørgaard Samuelsen, Jiri Srba

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

5 Citationer (Scopus)

Abstract

State-space explosion is a major obstacle in verification of time-critical distributed systems. An important factor with a negative influence on the tractability of the analysis is the size of constants that clocks are compared to. This problem is particularly accented in explicit state-space exploration techniques. We suggest an approximation method for reducing the size of constants present in the model. The proposed method is developed for Timed-Arc Petri Nets and creates an under-approximation or an over-approximation of the model behaviour. The verification of approximated Petri net models can be considerably faster but it does not in general guarantee conclusive answers. We implement the algorithms within the open-source model checker TAPAAL and demonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.
OriginalsprogEngelsk
TitelProceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14)
Antal sider15
Vol/bind8711
ForlagSpringer Publishing Company
Publikationsdato2014
Sider237-251
ISBN (Trykt)978-3-319-10511-6
ISBN (Elektronisk)978-3-319-10512-3
DOI
StatusUdgivet - 2014
Begivenhed12th International Conference on Formal Modeling and Analysis of Timed Systems - Florence, Italien
Varighed: 8 sep. 201410 sep. 2014
Konferencens nummer: 12

Konference

Konference12th International Conference on Formal Modeling and Analysis of Timed Systems
Nummer12
Land/OmrådeItalien
ByFlorence
Periode08/09/201410/09/2014
NavnLecture Notes in Computer Science (LNCS)
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets'. Sammen danner de et unikt fingeraftryk.

Citationsformater