Other formats:
BibTeX
LaTeX
RIS
@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 and 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, p.~237-251. ISBN~978-3-319-10511-6. Available from: https://dx.doi.org/10.1007/978-3-319-10512-3\_{}17.
|