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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00080035" target="_blank" >RIV/00216224:14330/14:00080035 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-10512-3_17" target="_blank" >10.1007/978-3-319-10512-3_17</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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 anover-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 anddemonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.

Název v anglickém jazyce

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

Popis výsledku anglicky

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 anover-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 anddemonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14)

ISBN

9783319105116

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

237-251

Název nakladatele

Springer-Verlag

Místo vydání

Nizozemsko

Místo konání akce

Italie

Datum konání akce

1. 1. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—