Improvements in Model Checking for Object-Oriented Petri Nets

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F04%3APU49209" target="_blank" >RIV/00216305:26230/04:PU49209 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Improvements in Model Checking for Object-Oriented Petri Nets
Original language description
Safety and liveness properties can be expressed by LTLX in model checking of a concurrent system. However, common logics, and LTLX is ranked among them, do not provide tools for tracing particular instances along state space paths. For this reason, an indexed temporal logic (ICTL) has been introduced into Object-Object Petri Net model checking.<br>Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we presenta new version of partial order reduction algorithm for LTLX in the context of Object-Oriented Petri Nets.
Czech name
Zlepšení v model checkingu objektově-orientovaných Petriho sítí
Czech description
Pro popis bezpečnosti a živosti ve verifikaci paralelních systémů se často používá lineární temporální logika (LTLX). Temporální logika však neumožňuje sledovat jednotlivé instance objektů podél cest stavového prosotru. Proto do verifikace objektově-orintovaných Petriho sítí byla zavedena indexovaná temporální logika (indexed temporal logic (ICTL)).<br>Verifikační nástroje se snaží redukovat počet navštívených stavů stavového prostoru. Pro model checking objektově-orientovaných Petriho sítí tento článeek prezentuje novou verzi algoritmu redukce stavového prostoru pomocí částečného uspořání.<br>

Project
<a href="/en/project/GA102%2F04%2F0780" target="_blank" >GA102/04/0780: Automated methods and tools supporting development of reliable concurrent and distributed systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2004
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
Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications
ISBN
980-6560-19-1
ISSN
—
e-ISSN
—
Number of pages
6
Pages from-to
269-274
Publisher name
The International Institute of Informatics and Systemics
Place of publication
Orlando
Event location
Orlando, Florida
Event date
Jul 21, 2004
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)