témavezető: Majzik István
helyszín (magyar oldal): Méréstechnika és Információs Rendszerek Tanszék helyszín rövidítés: MIT
A kutatási téma leírása:
Az informatikai rendszerekben bennmaradó szoftver hibák kockázatának növekedésével mindinkább elvárás az, hogy a kritikus funkciók tervezése és megvalósítása bizonyítottan helyes (hibamentes) legyen. Ennek egyik jellegzetes megoldása a formális módszereket alkalmazó fejlesztés: formális modellek biztosítják a követelmények és tervek egyértelmű és precíz rögzítését, ezeken formális verifikációval vizsgálhatók a tervezői döntések és bizonyíthatók a tervek egyes tulajdonságai. A formális verifikáció egyik legsikeresebb módszere a modellellenőrzés. Ennek során a tervezett rendszer állapotterén kimerítő módon történik temporális logikák segítségével formalizált tulajdonságok ellenőrzése. A modellellenőrzéshez az évek során számos technikát dolgoztak ki (pl. szimbolikus modellellenőrzés, korlátos modellellenőrzés), ezek nagyméretű állapottereken is képesek a specifikált tulajdonságok vizsgálatára. A verifikáció gyorsabb és kisebb erőforrásigényű végrehajtása azonban még mindig jelentős kutatási feladat.
A doktori kutatás célja új technikák kidolgozása a modellellenőrzés hatékonyságának és használhatóságának növelésére. Ennek során meg kell vizsgálni és ki kell dolgozni az utóbbi években felmerült új ötletek és módszerek (szaturáció, tulajdonság-orientált ellenőrzések, állapottér redukció) integrált alkalmazását. Ugyancsak jelentős előrelépést ígér a korlátozott (az állapotér meghatározott részén végezhető) absztrakció módszerének kidolgozása. A tulajdonságok szempontjából elvárás mind lineáris, mind pedig elágazó idejű temporális logikák támogatása. A modellellenőrzés így adódó új algoritmusait úgy kell kiterjeszteni, hogy a tulajdonság megsértése esetén alkalmasak legyenek a hibakeresést segítő ellenpélda generálására. Szintén új megoldások szükségesek ahhoz, hogy az ellenpélda alapján automatikusan javaslatokat lehessen adni a modell módosítására.
A kutatás kapcsolódik az R5-COP nemzetközi kutatási projekthez valamint biztonságkritikus rendszerek fejlesztését célzó ipari projektekhez.
felvehető hallgatók száma: 1
Jelentkezési határidő: 2015-01-05
2024. IV. 17. ODT ülés Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).
Bejelentkezés
