Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HAŠA, L. ČEŠKA, M.
Originální název
Design of a Model Checker for Object-Oriented Petri Net Models
Typ
článek ve sborníku mimo WoS a Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
LTL\X, model checking, Object-Oriented Petri Nets, partial-oreder reduction, state space
Autoři
HAŠA, L.; ČEŠKA, M.
Rok RIV
2003
Vydáno
17. 10. 2003
Nakladatel
IPSI Belgrade Ltd
Místo
Belgrad
ISBN
88-85280-62-5
Kniha
IPSI-2003 Proceedings
Strany počet
6
BibTex
@inproceedings{BUT10902, author="Luděk {Haša} and Milan {Češka}", title="Design of a Model Checker for Object-Oriented Petri Net Models", booktitle="IPSI-2003 Proceedings", year="2003", pages="6", publisher="IPSI Belgrade Ltd", address="Belgrad", isbn="88-85280-62-5" }