Petri-háló modellek részleges rendezés alapú vizsgálata

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

Napjainkban elterjedtek a biztonságkritikus elosztott rendszerek. Ezen rendszerek helyes működése legtöbbször kritikus szempont. A helyes működésről többek között a napjainkban egyre elterjedtebb, precíz matematikai formalizmusokon alapuló formális módszerek használatával tudunk gondoskodni. Jelen szakdolgozat célja egy olyan eszköz készítése, amely elosztott, aszinkron rendszerek modelljeinek ellenőrzésére alkalmas. A fejlesztés során a PetriDotNet keretrendszerbe egy verifikációs modult készítettem, amely Petri-hálók részleges rendezés alapú vizsgálatát teszi lehetővé. Választásom a kiterítés alapú, úgynevezett unfolding algoritmusra esett, amely sok olyan modell vizsgálatát lehetővé teszi, amiket más, egyszerűbb algoritmusok nem tudnak elvégezni. Megoldásom két részre bontható: először elkészítem a modell állapottér-reprezentációját, majd ezt egy kielégíthetőségi problémára képezem le, amit beadok egy külső megoldónak. Az elkészített eszközhöz készítettem egy egyszerű felhasználói felületet is, amely biztosítja a könnyű kezelhetőséget.

Letölthető fájlok

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