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

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F03%3APU42621" target="_blank" >RIV/00216305:26230/03:PU42621 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

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 reductionns. 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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA102%2F01%2F1485" target="_blank" >GA102/01/1485: Enviroment for development, modelling and application of heterogenous systems</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2003

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

IPSI-2003 Proceedings

ISBN

88-85280-62-5

ISSN

—

e-ISSN

—

Number of pages

6

Pages from-to

0-5

Publisher name

IPSI Belgrade Ltd

Place of publication

Belgrad

Event location

Svatý Štefan, Černá Hora

Event date

Oct 4, 2003

Type of event by nationality

EUR - Evropská akce

UT code for WoS article

—