 |
|
| Témakiírás |
| |
A kutatási téma leírása:
A téma részletesebb leírása:
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 együtt 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 az ilyen rendszerekkel kapcsolatos elvárások is folyamatosan nőttek, 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 mind a tervezési/fejlesztési, mind a gyártási és telepítési fázisban nagy hangsúlyt kell fektetni 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 alkalmazni, 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ök, 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 az extrafunkcionális, pl. teljesítőképesség, 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 (tesztelési) és a diagnosztikai feladatokat is támogatni tudja (pl. automatikusan generált tesztek formájában).
A formális módszerek bevonása tehát a közlekedési rendszerek fejlesztési életciklusának minél korábbi fázisaiba 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.
a) Előzmények:
A verifikációs és validációs eljárások támogatása formális módszerek alkalmazásával jelenleg is kihívást jelentő kutatási terület minden ipari alkalmazási területen (így a vasúti közlekedési rendszerek esetében is), amelynek éppen aktuális irányait a több évtizedre visszatekintő rendszeresen megrendezésre kerülő szimpóziumok (FME, FORMS, NFM, ICFEM stb.) keretei között tárgyalják európai és nemzetközi szinten.
A vasúti közlekedési rendszerekre vonatkozó verifikációs és validációs eljárások támogatása formális módszerek alkalmazásával több közlekedéstudományokra szakosodott egyetemen vizsgálat tárgyát képezi (pl. Newcastle University, Technical University of Denmark, Griffith University, University of Florence).
Magyarországi viszonylatban a téma előzményét [1] képezi.
b) A kutatás célja:
A formális módszerek alkalmazási lehetőségeinek kutatása a vasúti közlekedési rendszerek verifikációs és validációs folyamatainak támogatása céljából, az alkalmazható specifikációs, modellezési és analízis technológiák kiválasztása, és (amennyire jelenleg lehetséges) egységes ellenőrzési eszközkészletbe szervezése.
c) Az elvégzendő feladatok, azok fő elemei, időigénye:
A kutatás tervezett időigénye 3-4 év.
Fő feladatok (az egyes részfeladatok időben átlapolódnak, önálló időigény megadása nem célszerű).
– Irodalomkutatás: alkalmazható formális specifikációs, modellezési és analízis módszerek számbavétele és a kapcsolódó gyakorlati alkalmazási tapasztalatok értékelése a vasúti rendszerek életciklus fázisainak tekintetében.
– Egy konkrét alkalmazási környezet (pl. gyakorlatban fejlesztett berendezés/berendezéscsalád) kiválasztása és az értékelt formális módszerek közül a kiválasztott alkalmazási környezet fejlesztési, megvalósítási, gyártási és üzemeltetési folyamataihoz illeszkedő formális módszerek kiválasztása.
– Az alkalmazási környezetben konkrét formális specifikációk, modellek és analízis eredmények készítése. A tapasztalatok alapján a felhasznált formális módszerek értékelése, szükség esetén újabb módszerek bevonása.
– Az elméleti háttér és a gyakorlati tapasztaltok alapján a konkrét alkalmazási környezet verifikációs és validációs feladatainak számára a formális módszerek egységes metodikába/eszközrendszerbe szervezése. A vasúti közlekedési rendszerek területére általánosítható útmutatások kidolgozása.
d) A szükséges berendezések:
A kutatás a témából adódóan tisztán elméleti jellegű, csak szoftver eszközöket igényel. A szükséges számítástechnikai eszközök és szakmai anyagok rendelkezésre állnak.
e) Várható tudományos eredmények:
– A biztonságkritikus vasúti közlekedési rendszerek fejlesztési életciklusához kapcsolódó verifikációs és validációs folyamatok formális módszerek alkalmazásával történő ipari alkalmazási lehetőségeit összefogó metodika.
– A formális módszerekkel nem reprezentálható verifikációs és validációs folyamatokkal való összefüggések azonosítása és vizsgálata.
– A kidolgozott eszközkészlet gyakorlati alkalmazása egy vasúti közlekedési berendezés(család) fejlesztése során, a tapasztalatok értékelése.
f) Irodalom:
[1] Sághi Balázs: Formális módszerek alkalmazása a vasútbiztosító technikában, PhD értekezés, 2003
[2] Jean-Francois Monin, M.G. Hinchey: Understanding Formal Methods, ISBN 9781852332471, 2003
[3] Pataricza András: Formális módszerek az informatikában, ISBN 9789639548909, 2006.
[4] Boca, Paul, Bowen, Jonathan P., Siddiqi, Jawed (Eds.): Formal Methods: State of the Art and New Directions, ISBN 9781848827363, 2010.
[5] Jean-Louis Boulanger: Industrial Use of Formal Methods: Formal Verification, ISBN 9781848213630, 2013.
[6] Jean-Louis Boulanger: Formal Methods Applied to Industrial Complex Systems, ISBN: 9781848216327, 2014.
[7] Ferrari, Alessio; Fantechi, Alessandro;Gnesi, Stefania;Magnani, Gianluca: Model-Based Development and Formal Methods in the Railway Industry, Quality of Information and Communications Technology (QUATIC), International Conference, pp. 226-229, ISBN 9781479961320, 2014.
[8] Alessandro Fantechi, Francesco Flammini, Stefania Gnesi: Formal methods for railway control systems, International Journal on Software Tools for Technology Transfer, Vol. 16. pp. 643-646, 2014.
[9] Hao Cai, Chengdian Zhang, Weihang Wu, Tin-kin Ho, Zaiming Zhang: Modelling High Integrity Transport Systems by Formal Methods, Procedia - Social and Behavioral Sciences, Vol. 138, pp. 729–737, 2014.
előírt nyelvtudás: angol
felvehető hallgatók száma: 2
Jelentkezési határidő: 2017-10-12 |
|
|
|
|
Bejelentkezés
