Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail projektu
Období řešení: 01.01.1999 — 31.12.2000
O projektu
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.
Popis anglickyThis 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.
Klíčová slovaPetriho sítě - objektová orientace - temporální logiky - formální verifikace - stavová exploze
Klíčová slova anglickyPetri nets - object orientation - temporal logics - formal verification - state space explosion
Označení
FR1092/1999/G1
Originální jazyk
čeština
Řešitelé
Janoušek Vladimír, doc. Ing., Ph.D. - hlavní řešitelVojnar Tomáš, prof. Ing., Ph.D. - spoluřešitel