Conference paper

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.
Publication language:english
Original title:Design of a Model Checker for Object-Oriented Petri Net Models
Proceedings:IPSI-2003 Proceedings
Conference:Internet, Processing, Systems, Interdisciplinaries - VIP Forum
Place:Belgrad, YU
Publisher:IPSI Belgrade Ltd
LTL\X, model checking, Object-Oriented Petri Nets, partial-oreder reduction, state space
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.
   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 = {}

Your IPv4 address:
Switch to https