Detail publikace

Improvements in Model Checking for Object-Oriented Petri Nets

HAŠA, L., ČEŠKA, M. Improvements in Model Checking for Object-Oriented Petri Nets. In Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications. Orlando: The International Institute of Informatics and Systemics, 2004. p. 269-274. ISBN: 980-6560-19-1.
Název česky
Zlepšení v model checkingu objektově-orientovaných Petriho sítí
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Haša Luděk, Ing.
Češka Milan, prof. RNDr., CSc.
Klíčová slova

LTL, ICTL, model checking, objektově orientované Petriho sítě, redukce stavového prostoru

Abstrakt

Pro popis bezpečnosti a živosti ve verifikaci paralelních systémů se často používá lineární temporální logika (LTL\X). 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)).
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ánek prezentuje novou verzi algoritmu redukce stavového prostoru pomocí částečného uspořání.

Rok
2004
Strany
269–274
Sborník
Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications
ISBN
980-6560-19-1
Vydavatel
The International Institute of Informatics and Systemics
Místo
Orlando
BibTeX 
@inproceedings{BUT17351,
  author="Luděk {Haša} and Milan {Češka}",
  title="Improvements in Model Checking for Object-Oriented Petri Nets",
  booktitle="Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications",
  year="2004",
  pages="269--274",
  publisher="The International Institute of Informatics and Systemics",
  address="Orlando",
  isbn="980-6560-19-1"
}
Nahoru