Detail publikace

Improvements in Model Checking for Object-Oriented Petri Nets

ČEŠKA Milan a HAŠA Luděk. 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, s. 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
angličtina
Autoři
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Haša Luděk, Ing. (UITS FIT VUT)
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
Konference
International Conference on Cybernetics and Information Technologies, Systems and Applications: CITSA 2004, Orlando, Florida, US
ISBN
980-6560-19-1
Vydavatel
The International Institute of Informatics and Systemics
Místo
Orlando, US
BibTeX 
@INPROCEEDINGS{FITPUB7548,
   author = "Milan \v{C}e\v{s}ka and Lud\v{e}k Ha\v{s}a",
   title = "Improvements in Model Checking for Object-Oriented Petri Nets",
   pages = "269--274",
   booktitle = "Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications",
   year = 2004,
   location = "Orlando, US",
   publisher = "The International Institute of Informatics and Systemics",
   ISBN = "980-6560-19-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7548"
}
Nahoru