Matlab Simulink rendszerek modellalapú validációja

OData támogatás
Konzulens:
Dr. Horváth Ákos
Méréstechnika és Információs Rendszerek Tanszék

A beágyazott, biztonságkritikus rendszerek fejlesztése során kiemelt fontosságú a tervezett rendszer működésének tervezés idejű ellenőrzése. Ezek a rendszerek általában a környezetükkel interakcióba lépve végzik feladataikat, amely beavatkozók irányítását jelenti az érzékelők által végzett megfigyelések alapján. A tervezési idejű ellenőrzés során a környezet szimulációjával adatokat szolgáltatunk az érzékelőknek a beavatkozók kimenetei és előre meghatározott környezeti adatok alapján, eközben figyeljük a rendszer belső állapotát és működését.

A Matlab-Simulink a beágyazott, biztonságkritikus rendszerek fejlesztésében széles körben elterjedt modellezési és szimulációs eszköz. A Simulink segítségével lehetőség van komplex rendszerek hierarchikus megvalósítására és a rendszer komponenseinek szimulációjára. Azonban a Simulink általános modellezési megközelítése miatt nehézkes ellenőrizni, hogy az elkészített modellben található komponensek megfelelnek-e a tervezett rendszer felépítésére előírt strukturális kényszereknek. Ezen kényszerek gyakran gráf jellegű megkötéseket írnak elő a tervezendő rendszer architektúrájára, amiket nehézkes átláthatóan, imperatív módon specifikálni.

A szakdolgozat keretében egy olyan módszert valósítottunk meg, amelyben a Simulink modellekre vonatkozó rendszervalidációs kényszerek deklaratív módon definiálhatók, és ezen kényszerek teljesülése tetszőleges Simulink modellen ellenőrizhető. A megoldásunk két lehetőséget ajánl ennek megvalósítására.

Egyik módszer, hogy a Simulink modelleket átalakítjuk az Eclipse Modeling Framework által használt reprezentációra, majd az EMF-IncQuery modell lekérdező eszköz segítségével végezzük el a validációt. A modell reprezentáció hatékonyságának és a lekérdező eszköz inkrementális működésének köszönhetően a módszer képes akár százezres méretű Simulink modellekre is skálázódni. A kialakított eszköz képes a modell lekérdező által szolgáltatott eredményeket a Simulink felhasználói felületén megjeleníteni.

A másik választás a deklaratív szabálydefiníciókból ellenőrző imperatív Matlab függvények generálása. Erre a célra az úgynevezett local-search alapú keresési technikák módszertanát használtuk fel, ellentétben a dolgozatban bemutatott másik módszer inkrementális megközelítésével. Ekkor, mindössze a szabályok megadását leszámítva, a teljes ellenőrzési folyamat a generált kód felhasználásával már közvetlenül a Simulink modelleken Matlab segítségével történik.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.