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

Lukács Gábor, Farkas Balázs


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

 

Vasúti biztosítóberendezések tervezésének formális modellezése Petri-hálók alkalmazásával: vágányutak azonosítása T-invariánsok felhasználásával

Farkas Balázs, Bartha Tamás

IFFK 2021

 

Construction of Formal Models and Verifying Property Specifications through an Example of Railway Intelocking Systems

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)

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

Az oldalon sütiket használunk
Weboldalunkon „cookie”-kat (továbbiakban „süti”) alkalmazunk. Ezek olyan fájlok, melyek információt tárolnak webes böngészőjében. Ehhez az Ön hozzájárulása szükséges. A „sütiket” az elektronikus hírközlésről szóló 2003. évi C. törvény, az elektronikus kereskedelmi szolgáltatások, az információs társadalommal összefüggő szolgáltatások egyes kérdéseiről szóló 2001. évi CVIII. törvény, valamint az Európai Unió előírásainak megfelelően használjuk.Azon weblapoknak, melyek az Európai Unió országain belül működnek, a „sütik” használatához, és ezeknek a felhasználó számítógépén vagy egyéb eszközén történő tárolásához a felhasználók hozzájárulását kell kérniük.