Monitorszintézis temporális követelmények alapján ROS környezethez

OData támogatás
Konzulens:
Dr. Majzik István
Méréstechnika és Információs Rendszerek Tanszék

A projekt célja, hogy gyakorlati megvalósítást mutasson a futásidőben végzett követelmény ellenőrzésre a Robot Operating System (ROS) rendszerben alacsony erőforrásigény mellett. Az ROS egy nyílt forráskódú platform, amelynek célja, hogy az ipari automatizálási feladatokat és a robotok szoftvereinek fejlesztését egyszerűbbé tegye.

Megvalósításhoz egy monitoralkalmazást készítettem, amit beillesztve egy meglévő ROS rendszerbe, ellenőrizni tudja azt, és amennyiben a megadott követelményeket megsértette vagy teljesítette az adott rendszer úgy az ennek megfelelő parancsokat tudja futtatni, ami jelentheti megsértés esetén a rendszer leállítását is. Az monitoralkalmazást dinamikusan generálom a megadott követelmények alapján, így biztosítva, hogy csak a legszükségesebb komponenseket.

A követelmény Linear Temporal Logic (LTL) kifejezésként kerül átadásra a generátor számára. Az LTL egy leíró nyelv, amely segítségével egymást követő elemi események sorrendjére határozhatunk meg kritériumokat, követelményeket. Ebből a követelményből a Generátor átalakítások és optimalizálások után elkészíti a monitoralkalmazás forráskódját, ami az elemi események meghatározásán kívül képes az ellenőrzés elvégzésére. Az elemi események meghatározását a generálás után kézzel kell elkészíteni, mivel a Generátor nem tudja meghatározni, hogy a rendszer például akkumulátor töltöttségi szintjét mi alapján határozza meg, továbbá hol és milyen formában érhető el az adat. Az események meghatározására szolgáló kód megírása az alkalmazásfejlesztő feladata. ROS rendszerben az üzenetek publisher-subscriber minta szerint kerülnek kihirdetésre, ami a gyakorlatban azt jelenti, hogy az alkalmazásfejlesztőnek tudnia kell, hogy mely topicokon érhetőek el az ellenőrzéshez szükséges adatok és azokra feliratkozva, megfelelő szűrők és logikai műveletek után előállítja az elemi eseményeket. Ezek után megtörténhet az ellenőrzés úgynevezett logikai kiértékelő blokkok segítségével melyek mindig csak a kifejezés aktuális részét értékelik ki, ezzel is erőforrásokat spórolva.

Az elemi események meghatározása után a monitor készen áll a fordításra. Fordítás után az elkészült komponens beilleszthető a kész rendszerbe, és megkezdheti annak ellenőrzését.

Letölthető fájlok

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