Aszinkron rendszerek modellellenőrzése párhuzamos technikákkal

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

Kivonat

Napjainkban a biztonságkritikus rendszerekkel szemben támasztott fontos követelmény a tervezési helyesség magas fokú verifikálhatósága, azaz igazolhatósága. Erre gyakran formális módszereket használnak, amelyek közül a modellellenőrzés az egyik leginkább elterjedt. A modellellenőrzés folyamán kimerítő állapottér bejárással vizsgáljuk a rendszerrel szemben támasztott követelményeket. Aszinkron rendszerek esetén a formális viselkedést gyakran Petri-hálók segítségével, a rendszerrel szemben támasztott követelményeket pedig CTL temporális logikai kifejezésekkel fogalmazzák meg.

A formális verifikáció, és különösen a modellellenőrzés során gyakran probléma az állapottér drasztikus mérete. Ennek leküzdésére az irodalomban leginkább szimbolikus technikákat használnak. A legújabb kutatási eredmények azt mutatják, hogy aszinkron rendszerek esetén lehetőség van olyan fejlett algoritmusokat [1] használni, amelyek nagy hatékonysággal tudják tárolni, illetve bejárni az aszinkron rendszerek által kifeszített óriási állapottereket. Ezen algoritmusok hatékonyan felhasználhatóak a modellellenőrzés során is [2].

Ahogy egyre gyakoribbá válnak a többmagos processzorok, többprocesszoros gépek, jogos igényként merül fel, hogy a különböző szimbolikus technikák kihasználják ezeket a plusz erőforrásokat. A szimbolikus technikákon alapuló modellellenőrzést több munkában is próbálták párhuzamosítani [3], azonban a próbálkozások döntő többsége csak részsikereket ért el a felhasznált algoritmusok és adatstruktúrák szekvenciális jellemvonásai következtében. Munkám során célul tűztem ki, hogy egy már meglévő algoritmust hatékonyan megvalósítsak és további gyorsítási lépésekkel egészítsek ki. Ennek keretében a [3]-ban ismertetett párhuzamos szimbolikus állapottér bejáró algoritmushoz dolgoztam ki új zárolási mechanizmusokat és integráltam a Méréstechnika és Információs Rendszerek Tanszéken fejlesztett PetriDotNet [4] Petri háló modellező keretrendszerbe. Ennek eredményeképp nagyobb fokú párhuzamos futást tudtam elérni, amely további gyorsulásokhoz vezetett. A PetriDotNet keretrendszer tartalmaz továbbá egy, a CTL nyelven megfogalmazott specifikációs követelményeket ellenőrző modult. Munkám során ezt a modult is továbbfejlesztettem oly módon, hogy bizonyos logikai kifejezések kiértékelését párhuzamossá alakítottam.

Eredményeimet mérésekkel igazolom, amelyekben összehasonlítottam az általam megvalósított párhuzamos algoritmust annak szekvenciális változatával mind az állapottér-felderítés, mind a modellellenőrzés tekintetében.

[1] Ciardo G, Marmorstein R, Siminiceanu R.: The saturation algorithm for symbolic state-space exploration. International Journal on Software Tools for Technology Transfer., 8(1):4-25., 2005.

[2] Ciardo G., Simiceanu T.: Structural symbolic CTL model checking of asynchronous systems. Computer Aided Verification, LNCS 2725, 40-50, 2003.

[3] Ezekiel J, Lüttgen G, Siminiceanu R.: Can saturation be parallelised? On the parallelisation of a symbolic state-space generator. PDMC conference on Formal methods: Applications and technology., 331-346., 2006.

[4] PetriDotNet információs oldal: https://www.inf.mit.bme.hu/research/tools/petridotnet

Letölthető fájlok

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