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

D 2014

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

BIRCH, Sine V., Thomas S. JACOBSEN, Jacob J. JENSEN, Christoffer MOESGAARD, Niels N. SAMUELSEN et. al.

Základní údaje

Originální název

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

Autoři

BIRCH, Sine V. (208 Dánsko), Thomas S. JACOBSEN (208 Dánsko), Jacob J. JENSEN (208 Dánsko), Christoffer MOESGAARD (208 Dánsko), Niels N. SAMUELSEN (208 Dánsko) a Jiří SRBA (203 Česká republika, garant, domácí)

Vydání

Nizozemsko, Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14), od s. 237-251, 15 s. 2014

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Link

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00080035

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-10511-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-10512-3_17

Klíčová slova anglicky

timed-arc Petri nets; approximation; abstractions; verification

Štítky

firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 10. 4. 2015 08:46, Prof. Jiří Srba, Ph.D.

Anotace

V originále

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.

Citovat

BIRCH, Sine V., Thomas S. JACOBSEN, Jacob J. JENSEN, Christoffer MOESGAARD, Niels N. SAMUELSEN a Jiří SRBA. Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets. In Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14). Nizozemsko: Springer-Verlag, 2014, s. 237-251. ISBN 978-3-319-10511-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-10512-3_17.

@inproceedings{1297401,
   author = {Birch, Sine V. and Jacobsen, Thomas S. and Jensen, Jacob J. and Moesgaard, Christoffer and Samuelsen, Niels N. and Srba, Jiří},
   address = {Nizozemsko},
   booktitle = {Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14)},
   doi = {http://dx.doi.org/10.1007/978-3-319-10512-3_17},
   keywords = {timed-arc Petri nets; approximation; abstractions; verification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Nizozemsko},
   isbn = {978-3-319-10511-6},
   pages = {237-251},
   publisher = {Springer-Verlag},
   title = {Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets},
   url = {http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17},
   year = {2014}
}

TY  - JOUR
ID  - 1297401
AU  - Birch, Sine V. - Jacobsen, Thomas S. - Jensen, Jacob J. - Moesgaard, Christoffer - Samuelsen, Niels N. - Srba, Jiří
PY  - 2014
TI  - Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets
PB  - Springer-Verlag
CY  - Nizozemsko
SN  - 9783319105116
KW  - timed-arc Petri nets
KW  - approximation
KW  - abstractions
KW  - verification
UR  - http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17
L2  - http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17
N2  - 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.
ER  -

BIRCH, Sine V., Thomas S. JACOBSEN, Jacob J. JENSEN, Christoffer MOESGAARD, Niels N. SAMUELSEN a Jiří SRBA. Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets. In \textit{Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14)}. Nizozemsko: Springer-Verlag, 2014, s.~237-251. ISBN~978-3-319-10511-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-10512-3\_{}17.

Podrobný výpis o publikaci