Formális módszerekkel a jobb szabványokért: Az UML PSSM állapotgép-szemantika szabvány validációja
Az emberiség egyre komplexebb biztonságkritikus rendszereket készít, amelyeket már túlnyomó többségben szoftverek vezérelnek. Ezen rendszerek hibás működése katasztrofális következményekkel járhat, ezért új fejlesztési módszertanok váltak szükségessé a biztonság garantálására. Többek között ilyen a modellalapú rendszertervezés is, amely számos előnnyel rendelkezik a hagyományos módszerekhez képest.
A modellalapú rendszertervezéshez elengedhetetlenek a modellezési nyelvek, amelyekkel többek között a rendszer viselkedése is leírható. A mérnöki viselkedésmodellek esetében is egyre elterjedtebb a végrehajtható modellek használata, melyek haszna abban rejlik, hogy pontos végrehajtási szemantikával rendelkeznek. Reaktív rendszerek esetében széleskörben használt modellezési nyelv a Unified Modeling Language (UML) állapotgép formalizmusa, amely működésének leírását a Precise Semantics of UML State Machines (PSSM) szabvány definiálja. Az elvárt viselkedést egy tesztkészlet is bemutatja, amely tesztmodellek lehetséges lépéssorozatait definiálja. A szabvány minősége szempontjából kiemelten fontos, hogy ez a tesztkészlet a szöveges szemantikával konzisztens legyen, és hiánytalanul mutassa be a lehetséges viselkedések körét.
Ebben a dolgozatban formálisan modellezzük az UML állapotgépek PSSM szabvány által definiált működését, valamint a tesztkészlet állapotgépeit. Az így előálló modellekből formális módszerek segítségével automatizáltan előállítjuk a lehetséges lépéssorozatokat, melyeket végül összevetünk a szabványban megadottakkal. A bemutatott módszerrel lehetővé válik a szabvány esetleges hiányosságainak és hibáinak felfedése, amely a szabvány pontosításán keresztül segíti a jobb minőségű mérnöki modellek készítését, végső soron pedig a biztonságosabb kritikus rendszerek fejlesztését is.
szerzők
-
Szkupien Péter
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc) -
konzulensek
-
Elekes Márton
Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék -
Graics Bence
Tudományos segédmunkatárs, Méréstechnika és Információs Rendszerek Tanszék -
Dr. Molnár Vince
Adjunktus, Méréstechnika és Információs Rendszerek Tanszék
helyezés
Morgan Stanley II. helyezett