PLC kódok modellellenőrzése

A CERN (Európai Részecskefizikai Kutatóintézet) számos PLC-t (programozható logikai vezérlőt) használ ipari folyamatainak szabályozására. Az ezeket vezérlő programok helyességén sokszor drága berendezések illetve emberek biztonsága múlik, így fontos lenne, hogy működésüket formálisan ellenőrizzék. Ezt támogatja a CERN-ben fejlesztett PLCverif eszköz (http://cern.ch/enice/PLC+formal+verification).

A PLCverif egy olyan, Eclipse-alapú keretrendszer, amelyben az implementációt készítő mérnökök magas szinten, akár a háttérben futó ellenőrzési algoritmusok specialitásainak ismerete nélkül végezhetik az ellenőrzést. Ennek feltétele, hogy a felhasznált verifikációs eszközök (tipikusan modellellenőrzők) a felhasználótól elrejtve működjenek. A PLCverif egy jól dokumentált felületet nyújt a különböző modellellenőrzők becsatolására.

A hallgató feladata megismerkedni a PLCverif eszközzel, illetve különböző modellellenőrzők bemeneti nyelveivel, hogy aztán megfelelő bővítmények implementálásával új modellellenőrző(ke)t csatolhasson az eszközbe.

A témát a BME-n és a CERN-ben kutató doktoranduszok közösen konzultálják.

Kapcsólódó érdekesebb publikációk itt elérhetőek: http://cern.ch/plcverif/
Ezek közül leginkább a következő kapcsolódik a témához: https://cds.cern.ch/record/1956439/files/CERN-ACC-2014-0221.pdf