Detail publikace

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

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"
}