Result Details
Design of a Model Checker for Object-Oriented Petri Net Models
Češka Milan, prof. RNDr., CSc.
Verification should be a very important part in the development ofconcurrent systems. To simplify verification, automatic techniques andautomatic model checkers are developed. This paper presents a design ofa model checker for Object-Oriented Petri Net models. Object-OrientedPetri Net is modelling formalism that supports modelling of all keyfeatures of concurrent and distributed object-oriented systems. Thepresented model checker uses on-the-fly model checking compounded withstate space reductions. We consider verification of deadlockability,state invariants, and also verification against a class of global (notinstance-oriented) next-time-free linear-time temporal logic formulae.
LTL\X, model checking, Object-Oriented Petri Nets, partial-oreder reduction, state space
@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"
}