Tanszéki konzulens: 

Bartha Tamás docens Szoba: IB419 Tel.: +36 1 463-3594 Email: bartha (*) mit * bme * hu

A ipari rendszerek leírására elterjedtek a funkcionális blokkdiagram (FBD) alapú leírások. Ezek olyan grafikus modellek, amelyek jól áttekinthető és a rendszermérnökök számára könnyen kezelhető módon írják le az irányítástechnikai rendszer működését.

Sajnos a jelenlegi gyakorlatban a védelmi logikák automatikus formális helyességellenőrzése nem része a fejlesztési folyamatnak, ugyanis az FBD alapú leírások (ma még) nem alkalmasak formális verifikáció elvégzésére. A továbblépés egyik lehetősége, ha létrehozunk egy formális modellkönyvtárat és olyan kompozíciós módszereket, amelyekkel a folyamat- és irányítástechnikai mérnökök által funkcionális blokkdiagramok formájában leírt funkciók automatikusan, manuális munka igénye nélkül és ellenőrzötten helyes módon formális biztonságigazolásra és helyességbizonyításra alkalmas modellé alakíthatók.

Ez az automatikus ellenőrzési folyamat több lépésből áll, amelyek önmagukban is számos érdekes kérdést és megoldandó problémát vetnek fel:

1. A funkcionális blokkdiagram alapú (vagy más szabványos ipari) leírás (rendszer-/alrendszerterv) formális modellé alakítása
2. A rendszerrel szemben támasztott (biztonsági) kritériumok formális modellé alakítása
3. A formális analízis elvégzése
4. Az analízis eredményeinek elemzése, felfedett hiba esetén a hibával kapcsolatos információk "visszavetítése" a kiinduló ipari modellbe/leírásba.
5. A tesztelés és diagnosztika támogatása utomatikus teszgenerálási és diagnosztikai eljárásokkal.

A hallgató feladata egy választott formális modellhez (időzített automaták, tranzíciós rendszerek) a fent vázolt transzformáció valamely fázisának elméleti vagy gyakorlati kérdéseinek körüljárása, megvalósítása.