Formális módszerek kutatócsoport
Motiváció
A beágyazott irányítási és biztonsági rendszerek alkalmazása a közlekedési rendszerek területén nagy múltra tekint vissza, és napjainkban is dinamikusan fejlődik. A közlekedésben is egyre több területen és alkalmazásban bukkannak fel beágyazott rendszerek, amelyek tipikusan korszerű digitális architektúrára építkeznek, funkcionalitásukat döntően valamilyen szoftver határozza meg, és sok esetben kommunikációs kapcsolatokkal lazán csatolt, elosztott rendszert alkotnak. Az ilyen rendszerek lehetőségei sokat bővültek mind a funkcionalitás, mind a flexibilitás terén, ugyanakkor ez a komplexitás nagymértékű növekedésével is járt. Az összetett, sok különböző komponensből álló, nehezen áttekinthető felépítés pedig mind a tervezési hibák, mind az üzemeltetési fázisban bekövetkező hardver hibák valószínűségét is növeli.
Térhódításukkal párhuzamosan viszont az ilyen rendszerekkel kapcsolatos elvárások is folyamatosan nőnek, köszönhetően többek között a növekvő forgalomból származó megnövekedett kockázatnak. Különösen igaz ez a kötöttpályás közlekedésre, ahol mind az anyagi, mind az emberéleteket és a környezetet fenyegető kockázat jelentős. Ennek megfelelően az e rendszerektől elvárt kockázatcsökkentés, azaz az IEC 61508-as szabványcsalád (illetve a vasúti területre kidolgozott EN 50126, EN 50128-29) fogalmai szerint a biztonságintegritási szint (Safety Integrity Level, SIL) is magas lehet: a biztonsággal összefüggő területeken sok esetben a legmagasabb, SIL4-es szintet kell teljesíteniük. Ilyen magas követelmények teljesítéséhez a berendezésgyártóknak és a megoldásszállítóknak is mind a tervezési/fejlesztési, mind a gyártási és telepítési fázisban nagy hangsúlyt kell fektetniük az ellenőrzési (azaz a verifikációs és validációs, V&V) tevékenységekre. Ehhez olyan ellenőrzési metodikákat és technológiákat kell alkalmazniuk, amelyek szisztematikus folyamatot adnak; biztosítják az elvárt fedettséget mind az ellenőrzött működésre, mind a hibákra; esetleg egy korlátozott területen garantálni tudják a konzisztenciát, teljességet, helyességet. Egy ilyen, a már említett IEC 61508-as szabványcsalád által SIL3 szint alatt „recommended”, felette pedig „highly recommended” verifikációs eszközkészletet biztosítanak az ún. formális módszerek.
A formális módszerek olyan matematikai igényességű eszközöket jelentenek, amelyekkel precízen specifikálhatóak a rendszerrel szembeni követelmények (mind a funkcionális, azaz az elvárt működésre vonatkozó; mind a nem funkcionális, pl. rendelkezésre állás), elkészíthető és fokozatosan és konzisztensen finomítható a rendszer modellje, majd modellellenőrzés vagy automatikus tételbizonyítás segítségével igazolható (a modellre nézve) a specifikált követelmények teljesülése. A formális modell elvezethet (automatikus kódgenerálás segítségével) egészen a konkrét implementációig, valamint a validációs (konkrétan a tesztelési) és a diagnosztikai feladatokat is támogatni tudja (pl. modellellenőrzés esetén a felfedett ellenpéldákból automatikusan generált tesztek formájában).
A fentieknek megfelelően a formális módszerek alkalmazása a közlekedési rendszerek fejlesztési életciklusának minél korábbi fázisaiban több szempontból is előnyt jelent, hiszen minél későbbi fázisban történik egy szisztematikus (azaz specifikációs, tervezési, vagy implementációs) hiba felfedése, annál nagyobb volumenű munkát igényel és annál nagyobb költséggel jár annak kijavítása, nem beszélve a fel nem fedett hibák következményeiről. Ugyanakkor a formális módszerek alkalmazása magas szintű specializált tudást és komoly (mind emberi, mind számítási) erőforrás ráfordítást igényel. Ennek köszönhetően a formális módszerek alkalmazásának elterjedése (nem csak a vasúti közlekedési rendszerek területén) lassú. Jelenleg még kevés a tapasztalat, és nincs egységes megközelítés, amely teljes megoldást mutatna a vasúti közlekedési rendszerek verifikációs és validációs folyamataira vonatkozóan.
Oktatók
Dr. Bartha Tamás, Dr. Tarnai Géza
PhD hallgatók
Kutatási eredmények
Fejlesztés alatt!
Publikációk
Állomási főjelzők jelzési képeinek, valamint optikakiosztásának automatizált meghatározása
Farkas Balázs, Bozsóki Gergely
Vasúti Vezetékvilág 2022/4
Állomási főjelzők kialakításának és jelzési képeinek szisztematikus meghatározása
Farkas Balázs, Bartha Tamás
IFFK 2022
Automated Railway Interlocking Plan Verification Using Petri Nets
Farkas Balázs, Bartha Tamás
Railways 2022
Farkas Balázs, Bartha Tamás
IFFK 2021
Gábor Lukács, Tamás Bartha
Pollack Periodica, Vol. 14, No. 2, pp. 39-50 (2019), DOI: 10.1556/606.2019.14.2.4
Optimalizálási feladatok megoldása biztosítóberendezések tervezése során – 2. rész
Boldis Bálint, Farkas Balázs, Székely Béla
Vasúti Vezetékvilág 2019/2
Optimalizálási feladatok megoldása biztosítóberendezések tervezése során – 1. rész
Boldis Bálint, Farkas Balázs, Székely Béla
Vasúti Vezetékvilág 2019/1
CTL-alapú modellellenőrzés a vasút-automatikai rendszerek fejlesztésében
Lukács Gábor, Bartha Tamás
Közlekedésfejlesztési és beruházási konferencia, 2018
Biztosítóberendezések szakterületi formális specifikációinak előkészítése
Lukács Gábor, Bartha Tamás
INNORAIL 2017
Vasúti biztosítóberendezések formális specifikációjának formális modellre való automatizált transzformálásának lehetőségei
Lukács Gábor, Dr. Bartha Tamás
IFFK 2017
Követelmények formalizálásának tapasztalatai a vasúti biztosítóberendezés fejlesztésben
Lukács Gábor, Dr. Bartha Tamás, Farkas Balázs
IFFK 2017
Experiences with the Formal Modeling of the Geographical and Tabular Principles of Interlocking Systems
G. Lukács, B. Farkas, T. Bartha
21st International Scientific Conference TRANSPORT MEANS 2017
Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén – 2. rész
Farkas Balázs, Lukács Gábor, Dr. Bartha Tamás
Vasúti Vezetékvilág XXII. 2017/3
Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén – 1. rész
Farkas Balázs, Lukács Gábor, Dr. Bartha Tamás
Vasúti Vezetékvilág XXII. 2017/2
Szakdolgozatok és diplomatervek
Czakó Márk: Jelfogós áramkörök formális modellezése (2023)
- Összefoglaló (letöltés)
- Diplomaterv (letöltés)
Bozsóki Gergely: Vasúti biztosítóberendezések tervezését segítő módszerek kidolgozása (2022)
- Összefoglaló (letöltés)
- Szakdolgozat (letöltés)
- Program 1 (letöltés)
- Program 2 (letöltés)
Szalai Dániel: Megcsúszási függőségek tervezése formális módszerek segítségével (2021)
Zakar Gergely: Oldalvédelmi függőségek tervezése formális módszerek segítségével (2021)
Boldis Bálint: Optimalizálási feladatok megoldása vasúti biztosítóberendezések tervezése során (2018)
- Diplomaterv (letöltés)
Farkas Balázs: Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén (2016)