Regisztráció és bejelentkezés

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)
  • Zavada Ármin
    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
    Doktorandusz, 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