PINS.NET - Formális modellek egységes kezelése .NET környezetben

OData támogatás
Konzulens:
Molnár Vince
Méréstechnika és Információs Rendszerek Tanszék

A jelen szakdolgozatban kifejlesztésre került és bemutatott szoftverkomponens a biztonságkritikus rendszerek formális ellenőrzéséhez járul hozzá. Biztonságkritikus rendszerek esetén a helyesség bizo-nyítása alapkövetelmény. Ilyen rendszereknél a tesztelés által nyújtottnál erősebb garanciára van szük-ség. A rendszer terveinek formális ellenőrzése a fejlesztés korai fázisában, matematikai alapokon képes a tervezési hibák minimalizálására, elősegítve a magasabb megbízhatóságot és az alacsonyabb költsége-ket. A tervezési fázisban formális modelleket készítenek a rendszer tervezett viselkedéséről, majd eze-ket matematikai módszerekkel, jobb esetben automatizált algoritmusokkal elemzik.

Az automatikus megoldások közül az egyik lehetőség a már bevált és elfogadott modellellenőrző eljá-rások használata. A probléma megoldására számos algoritmus létezik, azonban sokféle formális model-lezési nyelv is kifejlesztésre került, ezek pedig ritkán kompatibilisek az algoritmusokkal. Implementáció szempontjából problémát jelent, hogy egy eszköz fejlesztőjének minden algoritmust potenciálisan mindegyik formalizmushoz implementálnia kell, ami a többletmunka mellett nagyobb hibalehetőséget is hordoz. A Linux operációs rendszerre írt LTSmin modellellenőrző eszköz úgy hidalja át ezt a problé-mát, hogy definiál egy közös interfészt az algoritmusok és a modellezési formalizmusok között, amely képes szétválasztani a modellezés és ellenőrzés problémáját, de még kellő mennyiségű információt hor-doz a specializált megoldásokhoz. Ez az interfész a PINS (Partitioned Next-State Interface), ami jó alapja lehet egy eszközök között is átívelő közös megoldásnak.

A Budapesti Műszaki és Gazdaságtudományi Egyetemen működő Hidatűrő Rendszerek Kutatócso-prot által fejlesztett PetriDotNet modellező és modellellenőrző szoftver szintén sokat profitálna a PINS interfész alkalmazásából. Ehhez azonban nem elég újraírni az interfészt az eszköz által használt C# nyelven, hanem az eredeti interfészt kell alkalmassá tenni .NET programokból történő használatra, ugyanis így a már illesztett modellezési formalizmusok azonnal használhatók lennének. A szakdolgozat célja ennek a feladatnak a megoldása volt, ami a .NET és a Linux-alapú megoldások összeférhetetlen-sége miatt komoly nehézségeket jelentett.

A feladatot végül sikerült úgy megoldani, hogy az LTSmin-PINS, és a hozzá készített .NET interfész egy folyamaton belül működjön. Ez – amellett, hogy az interfész mostantól a PetriDotNet eszközben is használható – lehetővé teszi, hogy a PINS.NET projekt bármilyen .NET alapú eszközbe beépíthető legyen. Járulékos eredményként készült egy natív, objektumorientált C++ interfész is, ami a Windows operációs rendszerre fordított C++ alkalmazások számára is elérhetővé teszi a komponenst.

A munka azonban még nem ért véget, mivel az elkészült kód egyelőre egy működő, de kezdetleges prototípus, ami egyfajta iránymutatás a folytatáshoz. A feladat neheze azonban – a technológiák össze-kapcsolása – már megoldásra került.

Letölthető fájlok

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