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.

Témacsoport: 
Ellenőrzés és tesztelés
Jelleg: 
Elméleti
Advisor: 
Tamás Bartha
TDK lehetőség: 
TDK lehetőség
Megismerhető technológiák: 
(Színezett) Petri hálók, UPPAAL, SAL
Állapot: 
Korábbi