Paraméterezett időzített rendszerek formális analízise

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

Paraméterezett időzített rendszernek olyan rendszert tekintünk, melynek működését bizonyos paraméterek által behatárolt időzítés határozza meg. Ezek a rendszerek gyakran biztonságkritikus környezetben üzemelnek, így igazoltan helyes működésüket formális módszerek alkalmazásával kell biztosítani. E diplomaterv áttekinti az egyik legsikeresebb formális módszer, a modellellenőrzés alapjait. Ezen felül ismerteti az e rendszerek modellezésére alkalmas időzített, valamint paraméteres időzített automaták elméletének alapjait. Bemutat továbbá egy modellalapú nyelvi keretrendszert, melynek szintaxisa alkalmas paraméterezett, időzített viselkedés közvetlen modellezésére; modelltranszformációkon, valamint logikai reprezentációra történő leképezésen alapuló szemantikája pedig lehetővé teszi a modell szimbolikus vizsgálatát. A megközelítés használhatóságát két példa demonstrálja: az első egy kanonikus példa, Fischer jól ismert kölcsönös kizárás algoritmusa, a másik pedig egy ipari esettanulmány, a Prolan SCAN protokolljának kapcsolatkezelése.

Letölthető fájlok

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