Ellenőrzési és modellezési technikák

Ellenőrzési és modellezési technikák

Vezető kutató: 
Majzik István

Kritikus rendszerek (pl. járművek, robotok, irányítórendszerek szoftvere) esetén egy-egy hibának akár katasztrofális következményei is lehetnek. Így nem engedhető meg, hogy a hibákat csak a használat során vegyük észre, és utólag próbáljuk javítani. A fejlesztés minden fázisában szükség van olyan precíz modellezési és ellenőrzési technikákra, amelyek hatékonyan biztosítják a fejlesztett rendszer helyes és biztonságos működését.

A specifikáció és a tervek készítésének fázisában az ellenőrzéshez hátteret adnak a precíz, modell alapú tervezési és verifikációs módszerek. A forráskód készítés során az ellenőrzés statikus analízis eszközökkel történhet. A teszttervezés is hatékonyan támogatható ezekkel a technikákkal.  A hibavédelem utolsó bástyái pedig a futásidőbeli monitorok, amelyek véletlen hardver hibák esetén is képesek a biztonsági problémákat felismerni és beavatkozást indítani. Ezeken a területeken jelentős kihívásokat támasztanak az intelligens algoritmusokat alkalmazó korszerű rendszerek (pl. önvezető járművek, autonóm robotok, tanuló és adaptív rendszerek): hogyan tudjuk ezek helyességét és biztonságos működését ellenőrizni?

Az ellenőrzés mellett olyan kérdésekkel is foglalkozunk, mint az ellenőrzött tervek és modellek alapján történő szoftverkód generálás, illetve adott feltételeknek megfelelő modellek automatikus előállítása (pl. teszteléshez szükséges konfigurációk esetén), valamint a tervezők közti csoportmunka támogatása. Ezekkel a technikákkal jelentősen növelhető a fejlesztés hatékonysága.

A témacsoport keretében tehát - a tervezők és fejlesztők számára egyre inkább nélkülözhetetlen - modellezési és ellenőrzési eszközökkel és módszerekkel lehet megismerkedni, valamint ilyenek alkalmazásába lehet bekapcsolódni.

A lehetséges témalaboratórium és önálló laboratórium feladatok keretében hallgatóink foglalkozhatnak például eszközfejlesztéssel (akár csatlakozva már meglévő fejlesztői csapatokhoz, pl. Gamma, Theta, PetriDotNet, VIATRA 2 és EMF-IncQuery), az ellenőrzéshez szükséges hatékony algoritmusokkal, demo rendszereinkkel (pl. MODES3) vagy éppen (ipari partnereink által javasolt) konkrét modellezési és ellenőrzési feladatokkal.

A feladatcsoport tipikus témái:

  • Biztonságkritikus szoftverek (autó, repülő, vasúti alkalmazások) fejlesztésének megismerése,
  • Tervek és modellek helyességének ellenőrzése,
  • Szoftverek (forráskód) hibáinak felderítése,
  • Ellenőrző eszközök fejlesztése, ezekhez új algoritmusok és technikák kitalálása, megvalósítása,
  • Monitorok fejlesztése autonóm működésű rendszerekhez,
  • Adaptív és dinamikus architektúrájú rendszerek analízise.
 
Megismerhető technológiák: 
  • Követelmények precíz leírása (forgatókönyvek, LSC, MSC, temporális logikák) és követelménykezelés (DOORS)
  • Modell alapú tervezés: Petri-hálók, időzített automaták, állapottérképek (PetriDotNet, UPPAAL eszközök)
  • Modellek automatikus ellenőrzése (PetriDotNet, nuSMV, SAL, SCADE)
  • Tervezési minták hibatűréshez (redundancia, átkonfigurálás)
  • Forráskód ellenőrzés (PMD, FindBugs)
  • Futásidejű monitorozás (MOP, Eagle, RuleR)
  • Biztonságkritikus rendszerek fejlesztési szabványai (vasúti és autóipari alkalmazások)
  • Ellenőrzési eszközláncok, verifikációs és validációs folyamatok tervezése (SPEM, BPMN)
  • EclipseEclipse alapú technógiák és rendszerek
  • Modern programozási nyelvek (Xtend, Kotlin, Scala)
  • Rendszertervező eszközök (MagicDraw, Capella)
  • A tanszék saját fejlesztésű, nyílt forrású technológiái (VIATRA)
  • Machine-to-machine és Internet-of-Things technológiák
  • Szabálymotorok (Drools)
  • Mobil alkalmazásfejlesztés és fejlesztőeszközök (Android, iOS, ...)
  • Meta Programming System

Folyamatban levő témák

Cím Konzulensek
Modellvasút vezérlőszoftver modell alapú fejlesztése Vörös András
Nagyméretű aszinkron rendszerek korlátos modellellenőrzése Vörös András
PetriDotNet Vörös András
Kombinált explicit és implicit állapottér felderítő és modellellenőrző algoritmusok fejlesztése, implementálása Vörös András
Absztrakciós módszerek a modellellenőrzésben Vörös András
Absztrakt interpretáció alapú verifikáció Vörös András
Időzített rendszerek ellenőrzése Vörös András
PLC kódok modellellenőrzése
Ellenőrző kódrészletek illesztése C programokhoz Majzik István
Modellvasút vezérlőszoftver fejlesztése elosztott, beágyazott környezetben Vörös András
Modellellenőrző módszerek és algoritmusok összehasonlítása, mérési kampányok tervezése Vörös András
Autonóm rendszerek működésének futásidőbeli ellenőrzése Majzik István
Hibaterjedési vizsgálatok üzleti folyamat alapú rendszerekben Gönczy László
Szaturáció alapú Lineáris Temporális Logikai modellellenőrzés Vörös András
Lineáris tranzíciós rendszerek absztrakt interpretáció alapú verifikációja Vörös András
Monitor generálás temporális logikai követelményekből Majzik István
Az LTSmin modellellenőrző vizsgálata és kiterjesztése Molnár Vince
Korszerű modellellenőrző eszközök felmérése (2 fő)
Részleges rendezéses redukció alkalmazása modellellenőrzésben Molnár Vince
Bejárási stratégiák és adatszerkezetek vizsgálata szimbolikus modellellenőrzésben Molnár Vince
Monitor generálás scenario alapú követelményekből Majzik István
Hierarchikus állapotgépek formális verifikációja
Komponens alapú rendszerek megbízhatósági analízise Majzik István
Autonóm robotok szimulátor alapú tesztelése
Kritikus protokollok modellezése Majzik István
Állapot-alapú mérnöki modellek formális verifikációja