Detail projektu

Temporální vlastnosti modelů popsaných objektově orientovanými Petriho sítěmi

Období řešení: 1. 1. 1999 – 31. 12. 2000

Typ projektu: grant

Kód: FR1092/1999/G1

Název anglicky

Temporal Properties of Models Described by Object-Oriented Petri nets

Typ

grant

Klíčová slova

Petriho sítě - objektová orientace - temporální logiky - formální verifikace -
stavová exploze

Abstrakt

Cílem projektu je výzkum v oblasti formální analýzy a verifikace na modelech
popsaných objektově orientovanými Petriho sítěmi (OOPN), spojenými s nástrojem
PNtalk. To zahrnuje návrh vhodného specifikačního jazyka pro popis zkoumaných
vlastností modelů a metod jejich pokud možno efektivního ověřování s využitím
stavových prostorů OOPN. Řešení projektu bude probíhat zejména v rovině
teoretické, přesto by mělo dojít k alespoň pokusné implementaci některých
myšlenek v jazyce Prolog.

Řešitelé

Janoušek Vladimír, doc. Ing., Ph.D. (UITS) – hlavní řešitel
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)