Temporális logikai specifikációk vizsgálata

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

Biztonságkritikus rendszerek hibái akár katasztrofális következményekkel

járhatnak, ezért kiemelt fontosságú a helyes működés biztosítása. Annak

igazolásához, hogy a fejlesztett rendszer a specifikációnak megfelelően, hiba

nélkül működik, célszerű formális módszereket alkalmazni. Egy ilyen módszer a

modellellenőrzés, aminek segítségével még tervezési időben kiszűrhetőek az

esetleges hibák. Modellellenőrzés során a rendszer modelljén vizsgáljuk az

úgynevezett temporális logikák segítségével megfogalmazott követelmények

teljesülését. Több féle temporális logika létezik, dolgozatomban a lineáris

temporális logikán (LTL) alapuló modellellenőrzéssel foglalkozom.

Amennyiben egy vizsgált követelmény nem teljesül a modellen, az ellenőrzés

eredményeképp kapunk egy ellenpéldát, aminek birtokában lehetőségünk van a hiba

javítására. Ezzel szemben ha a követelmény teljesül a modellen, nem kapunk

információt a teljesülés módjáról. Ez azért jelent problémát, mert

gyakran előfordul, hogy a temporális logikai kifejezés hibás megfogalmazása

miatt triviális módon teljesül egy követelmény, így az esetleges hibára nem

derül fény.

A hibásan megfogalmazott követelmények felismerésére az egyik módszer az

LTL-kifejezések úgynevezett vacuity értékeinek vizsgálata, ami arról ad

információt, hogy a kifejezés mely részei feleslegesek a követelmény

teljesülésének szempontjából.

Dolgozatomban bemutatok egy vacuity értékek vizsgálatán alapuló módszert, ami

segítségével figyelmeztethetjük a felhasználót ilyen típusú hibák esetén is. Ez

után ismertetem a módszer egy általam egyszerűsített változatát is, melynek

implementációját elkészítettem a PetriDotNet modellellenőrző keretrendszer

részeként.

Letölthető fájlok

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