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
Pages:6
Proceedings:IPSI-2003 Proceedings
Conference:Internet, Processing, Systems, Interdisciplinaries - VIP Forum
Place:Belgrad, YU
Year:2003
ISBN:88-85280-62-5
Publisher:IPSI Belgrade Ltd
Keywords
LTL\X, model checking, Object-Oriented Petri Nets, partial-oreder reduction, state space
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=7316}
}

Your IPv4 address: 54.166.133.84
Switch to https

DNSSEC [dnssec]