Követelmény alapú monitorszintézis Android platformra

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

A projekt célja Android platformon futó alkalmazások viselkedésének ellenőrzéséhez, valamint a megfigyelhető eseményszekvenciák alapján történő aktív beavatkozáshoz szükséges monitor alkalmazás előállítása automatizáltan, a specifikált követelmények alapján. A követelmények leírása Lineáris Temporális Logikával (LTL), mint formális követelmény-specifikációs nyelv segítségével történik, a megfogalmazott LTL kifejezés operandusai a megfigyelhető események halmazának elemei, operátorai pedig temporális és Boole-logikai operátorok. Az elkészített Java-alapú kódgenerátor alkalmazás egy LTL kifejezést kap bemenetként, kimenete pedig egy Android platformon futtatható monitor alkalmazás, mely képes ellenőrizni a megfogalmazott kifejezés által leírt követelmény teljesülését, illetve sérülését, valamint igény szerint beavatkozhat a megfigyelt alkalmazás működésébe, például a követelmények megsértése esetén terminálhatja azt.

Alapvető követelmény, hogy az így előállított monitor, valamint az általa megfigyelt alkalmazás képes legyen kommunikálni egymással. Erre a célra egy köztes kommunikációs réteg került megvalósításra, melynek központi eleme egy olyan modul, melyhez az említett végpontok csatlakozhatnak, és anélkül kommunikálhatnak, hogy közvetlenül azonosítaniuk kellene egymást. A kommunikáció az ún. publisher-subscriber mintára épül, ez kézenfekvő, hiszen a minta sajátossága, hogy egy adott publisher által publikált eseményre több subscriber is feliratkozhat, így egy alkalmazást több monitor is megfigyelhet azonos időben, eltérő követelményeket vizsgálva. A központi modul a kliensek regisztrációja során hozzá eljuttatott információk, és az általa tartalmazott üzleti logika alapján képes kiszolgálni a végpontokat. A megfigyelt alkalmazás (mint eseményforrás) futása közben fellépő publikációs viselkedés tetszőlegesen konfigurálható, az alkalmazás ún. instrumentálásával, melynek során annak kódjában hívásokat helyezünk el egy szintén a projekt keretében készült, végpontokhoz társítható kapcsolattartó modulra. A modul egy olyan API-t nyújt az alkalmazások számára, mely segítségével képesek csatlakozni a központi modulhoz, eljuttatni számára a releváns információkat futásuk során, valamint képesek üzeneteket fogadni tőle. Az üzenetek feldolgozása kliens oldalon szintén instrumentációval történik, így a beérkezett üzenetek által kiváltott interakciók is testreszabhatóak.

Letölthető fájlok

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