Komponens-alapú reaktív rendszerek modellvezérelt tervezése és ellenőrzése
Manapság mindenhol körbevesznek minket biztonságkritikus rendszerek, amelyek helyes működésén emberéletek múlhatnak. Az utóbbi években rohamosan nőtt az ilyen rendszerek komplexitása, és ennek kezelésében egyre fontosabb szerepet kapnak a modell-alapú fejlesztési paradigmák. Ezek legfontosabb előnye, hogy a modellek nemcsak dokumentálják a komponenseket, hanem kódgenerálással az implementáció is automatikusan származtatható belőlük. Többféle eszköz és nyelv is rendelkezésre áll a rendszertervek elkészítésére, ezek közül a reaktív (környezetükre reagáló) rendszerek belső működésének ábrázolására általában állapot alapú modelleket használunk. A komponensek modelljeiből kompozíció segítségével lehet megalkotni a rendszer-szintű viselkedési modelleket. A kompozíciót támogató eszközök hiányossága azonban, hogy jellemzően nem definiálják pontosan a kompozíció szemantikáját, lehetetlenné téve az automatikus kódgenerálást. Ugyanezen okból a legtöbbször precíz validációt és verifikációt sem tesznek lehetővé.
Fontos szempont a biztonságkritikus rendszereknél, hogy a rendszer helyességét igazolni tudjuk. A tesztelés mellett ebben nagy szerep hárul a formális ellenőrzési módszerekre, amelyek nem csak a hibákat találják meg, de az elkészült rendszertervek helyességét is bizonyítani tudják. Állapot alapú viselkedés ellenőrzésére gyakran használt technika a modellellenőrzés. Sajnos a mérnöki modellezési formalizmusok jellemzően nem alkalmasak közvetlen analízisre, így a formális modelleket többnyire külön szakértő csapat készíti el.
Munkám célja egy olyan keretrendszer kifejlesztése, amely támogatja a mérnöki viselkedési modellek tervezését és ellenőrzését. Munkám alapjául egy köztes formális nyelv szolgál, erre építve definiáltam egy nyelvet, amely lehetővé teszi állapotgép modellek precíz szemantikájú kompozícióját. A keretrendszer része egy kódgenerátor, amely az állapotgép modellek implementációja és a kompozíciós nyelvben definiált szabályok mentén előállítja a komponált rendszer implementációját. A mérnöki modellezés támogatására validációs szabályokat definiáltam a köztes formális nyelvhez, amely elősegíti a tervezési hibák minél hatékonyabb kiszűrését. Emellett megvalósítottam a kompozit mérnöki modellek formális modellekre történő automatikus leképezését is, így lehetővé téve a tervek formális ellenőrzését.
A keretrendszerben a mérnöki állapot-alapú modellek tervezését pillanatnyilag egy elterjedten használt nyílt forráskódú állapotgép modellező eszköz, a Yakindu támogatja. A keretrendszerben modelltranszformációk segítségével definiáltam mind a mérnöki modellből a formális köztes modellbe, mind pedig a köztes modellből az UPPAAL modellellenőrző eszköz bemeneti formalizmusára való leképezést. A validációs szabályok tervezéséhez gráfminta-alapú szabályokat készítettem. A keretrendszer fontos előnye, hogy mind mérnöki modellező nyelvekkel, mind pedig formális ellenőrző eszközökkel tetszőlegesen bővíthető, így más tervező és analízis eszközökhöz is könnyen integrálható. A keretrendszer hasznosságát és működését a tanszéken fejlesztett, vasúti biztosítóberendezésekkel foglalkozó projekt segítségével demonstrálom.
szerző
-
Graics Bence
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
konzulensek
-
Dr. Molnár Vince
Adjunktus, Méréstechnika és Információs Rendszerek Tanszék -
Dr. Vörös András
egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék
