BIRCH, Sine V., Thomas S. JACOBSEN, Jacob J. JENSEN, Christoffer MOESGAARD, Niels N. SAMUELSEN and 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, p. 237-251. ISBN 978-3-319-10511-6. Available from: https://dx.doi.org/10.1007/978-3-319-10512-3_17.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets
Authors BIRCH, Sine V. (208 Denmark), Thomas S. JACOBSEN (208 Denmark), Jacob J. JENSEN (208 Denmark), Christoffer MOESGAARD (208 Denmark), Niels N. SAMUELSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution).
Edition Nizozemsko, Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14), p. 237-251, 15 pp. 2014.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW Link
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/14:00080035
Organization unit Faculty of Informatics
ISBN 978-3-319-10511-6
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-10512-3_17
Keywords in English timed-arc Petri nets; approximation; abstractions; verification
Tags firank_B
Tags International impact, Reviewed
Changed by Changed by: Prof. Jiří Srba, Ph.D., učo 2841. Changed: 10/4/2015 08:46.
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.
PrintDisplayed: 21/9/2024 21:46