Cím: 1111 Budapest, Stoczek u. 2.
 St. épület, 1. emelet 110

 E-mail: Ez az e-mail cím a spamrobotok elleni védelem alatt áll. Megtekintéséhez engedélyeznie kell a JavaScript használatát.

 Telefon: (36-1) 463-1013

mechatronika

kozut

vasut

legi

Kompetenciák

vasut

Ipari munkák

oktatas

>
Oktatás

vasut

Kutatás

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. Sághi Balázs, Dr. Tarnai Géza

PhD hallgatók

Lukács Gábor, Farkas Balázs


Kutatási eredmények

Fejlesztés alatt!


Publikációk (kéziratok)

Lukács Gábor, Dr. Bartha Tamás: 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, IFFK 2017

 

Lukács Gábor, Dr. Bartha Tamás, Farkas Balázs: Követelmények formalizálásának tapasztalatai a vasúti biztosítóberendezés fejlesztésben, IFFK 2017

 

G. Lukács, B. Farkas, T. Bartha: Experiences with the Formal Modeling of the Geographical and Tabular Principles of Interlocking Systems, 21st International Scientific Conference TRANSPORT MEANS 2017,

Proceedings: Part1, Part2, Part3, Part4, Part5, Part6

 

Farkas Balázs, Lukács Gábor, Dr. Bartha Tamás: Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén – 2. rész, Vasúti vezetékvilág XXII. 2017/3

 

Farkas Balázs, Lukács Gábor, Dr. Bartha Tamás: Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén – 1. rész, Vasúti vezetékvilág XXII. 2017/2


Szakdolgozatok és diplomatervek

Farkas Balázs: Formális modellezés alkalmazásának lehetőségei a vasúti biztosítóberendezések területén (2016)