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.

Description in English
This project is based on a research in the area of formal analysis and verification over models described by object-oriented Petri nets (OOPNs) associated to the tool called PNtalk. This research includes proposing a suitable specification language for specifying desired properties of systems modelled by OOPNs and methods of verifying them via state spaces of OOPNs in an as effective as possible way. The project is mostly theoretical, however, at least some of the obtained theoretical proposals will be checked via a prototype implementation in Prolog.

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

Key words in English
Petri nets - object orientation - temporal logics - formal verification - state space explosion