Időzített modellek ellenőrzése szaturációs algoritmussal

OData támogatás
Konzulens:
Vörös András
Méréstechnika és Információs Rendszerek Tanszék

Napjainkban általános sztereotípia, hogy a modern informatikai rendszerek jellemzően megbízhatatlanok. Ez a feltételezés azonban nem állhat fenn, ha olyan rendszerekről beszélünk, mint egy atomerőmű, egy repülőgép vagy egy szívritmus szabályzó. Utóbbiak közös jellemzője, hogy tervezésükre, forgalomba helyezésükre igen szigorú szabályok vonatkoznak, és működésük során a legkisebb hiba sem tolerálható. Kívánatos állapot lenne, ha az összes informatikai rendszer ezekhez hasonló rendelkezésre állási adatokkal bírna.

Hosszú idő óta folynak kutatások arra vonatkozóan, hogy az említett hibamentes működés biztosítható legyen. A rendszertervezés folyamatában ezt a lépést, amely a megtervezett rendszer helyességét vizsgálja, verifikációnak nevezik. Elvégzésére többféle módszer is rendelkezésre áll, ezek a kimerítő tesztelés, szimuláció, modellellenőrzés és a tételbizonyítás. Ezek közül én a modellellenőzéssel foglalkoztam kutatásaimban.

A modellellenőrzés során először a rendszertervek alapján egy matematikailag precíz modellt készítünk. Ezután bizonyítottan helyes algoritmusok segítségével felderítjük az elkészített modell állapotterét, és ellenőrizzük a specifikációs kritériumok teljesülését. Abban az esetben, ha az ellenőrzés során hibát fedeztünk fel, a rendszerterveket és modelleket módosítani kell, a kritériumok ellenőrzését pedig újra el kell végezni. Kutatásom célja az volt, hogy az időzített Petri-háló modellezési nyelvet kiegészítsem, hogy a valóságot jobban tükröző modelleket készíthessünk, valamint meglévő algoritmusokat továbbfejlesztve az eddigieknél szélesebb körben alkalmazhatóvá váljon a verifikáció.

Dolgozatomban bemutatom, hogy az időzített Petri-háló formalizmust új tranzíciótípusokkal egészítettem ki. A modellek ellenőrzésére két szaturáció [1] alapú algoritmust vizsgáltam meg alaposan. Az egyik a Timed Reachability [2], amely egy adott pillanatban elérhető állapotokat adja meg. A másik az Earliest Reacability [2], amely az összes elérhető állapotra megadja a legkorábbi elérési időket. Miután ezeket az algoritmusokat alaposan áttanulmányoztam, továbbfejlesztettem őket, hogy képesek legyenek az általam bevezetett új tranzíciótípusok kezelésére is. Munkám végén az algoritmusoknak elkészítettem az implementációját is. Erre a Budapesti Műszaki és Gazdaságtudományi Egyetem Méréstechnika és Információs Rendszerek Tanszékén fejlesztett PetriDotNet keretrendszert használtam.

[1] Gianfranco Ciardo, Gerald Lüttgen, and Radu Siminiceanu. Saturation: an efficient iteration strategy for symbolic state space generation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, pages 328–342. Springer-Verlag, 2001.

[2] MinWan and Gianfranco Ciardo. Symbolic reachability analysis of integer timed petri nets. In Mogens Nielsen, Antonín Kučera, PeterBro Miltersen, Catuscia Palamidessi, Petr Tůma, and Frank Valencia, editors, SOFSEM 2009: Theory and Practice of Computer Science, volume 5404 of Lecture Notes in Computer Science, pages 595–608. Springer Berlin Heidelberg, 2009.

Letölthető fájlok

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