Formálne metódy špecifikácie systémov

Vývoj novej metódy de/kompozičného návrhu , analýzy a verifikácie diskrétnych systémov založenej na integrovaných formálnych špecifikačných metódach (Petriho siete, B AMN, procesné algebry).

Koordinátor: prof. Ing. Štefan Hudák, DrSc.

• De/kompozičný návrh a analýza diskrétnych systémov založená na báze Petriho sietí.
• Tvorba novej teórie a metód de/kompozície Petriho sietí založenej na algebre PN termov. Sémantické vlastnosti PN termov: lingvistická a stavová sémantika. Štúdium relácií ekvivalencie a bisimulácie založenej na uvedených sémantikách.
• Komparatívne štúdie a integrácia formálnych špecifikačných metód: Petriho siete, automaty (B AMN), procesné s algebry.
• Verifikácia zložitých sieťových protokolov.
• Adaptácia mFDT prostredia na podporu semi-automatizovanej verifikácie návrhu systémov CPN.
• Vývoj novej metódy verifikáce návrhu systémov pomocou jazyka BAMN a JAVA založenej na CPN (Coloured Petri Nets) a na novom prístupe k analyze stavových priestorov neobmedzenej kardinality.