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)