Publication Details

Design of a Model Checker for Object-Oriented Petri Net Models

HAŠA Luděk and ČEŠKA Milan. Design of a Model Checker for Object-Oriented Petri Net Models. In: IPSI-2003 Proceedings. Belgrad: IPSI Belgrade Ltd, 2003, p. 6. ISBN 88-85280-62-5.
Type
conference paper
Language
english
Authors
Haša Luděk, Ing. (DITS FIT BUT)
Češka Milan, prof. RNDr., CSc. (DITS FIT BUT)
Keywords

LTL\X, model checking, Object-Oriented Petri Nets, partial-oreder reduction, state space

Abstract

Verification should be a very important part in the development of concurrent systems. To simplify verification, automatic techniques and automatic model checkers are developed. This paper presents a design of a model checker for Object-Oriented Petri Net models. Object-Oriented Petri Net is modelling formalism that supports modelling of all key features of concurrent and distributed object-oriented systems. The presented model checker uses on-the-fly model checking compounded with state space reductions. We consider verification of deadlockability, state invariants, and also verification against a class of global (not instance-oriented) next-time-free linear-time temporal logic formulae.

Published
2003
Pages
6
Proceedings
IPSI-2003 Proceedings
Conference
Internet, Processing, Systems, Interdisciplinaries - VIP Forum, Svatý Štefan, Černá Hora, YU
ISBN
88-85280-62-5
Publisher
IPSI Belgrade Ltd
Place
Belgrad, YU
BibTeX 
@INPROCEEDINGS{FITPUB7316,
   author = "Lud\v{e}k Ha\v{s}a and Milan \v{C}e\v{s}ka",
   title = "Design of a Model Checker for Object-Oriented Petri Net Models",
   pages = 6,
   booktitle = "IPSI-2003 Proceedings",
   year = 2003,
   location = "Belgrad, YU",
   publisher = "IPSI Belgrade Ltd",
   ISBN = "88-85280-62-5",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7316"
}
Back to top