Ipari biztonsági / védelmi rendszerek automatikus ellenőrzésének támogatása

Ipari biztonságkritikus rendszerekben a biztonsági beavatkozásokat indító ún. védelmi logikák tipikus leírási "nyelve" a funkcionális blokkdiagramok valamelyik változata. Ezek grafikus, könnyen áttekinthető leírását adják a megvalósítandó biztonsági funkciónak.

Sajnos a jelenlegi gyakorlatban a védelmi logikák automatikus formális helyességellenőrzése nem része a fejlesztési folyamatnak. 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.

A hallgató feladata egy kiválasztott formális modellezési nyelven (pl. Petri hálók, időzített automaták, tranzíciós rendszerek) kidolgozni néhány kiválasztott funkcionális blokk vagy tipikus logikai séma formális modelljét.