Szimbolikus modellellenőrzés és végrehajtási szekvencia generálás vezérelt kereséssel

A modellellenőrzés egy formális verifikációs technika, melynek feladata a rendszerrel szemben támasztott követelmények matematikailag precíz ellenőrzése a rendszer viselkedésmodelljén. A modellellenőrzés előnye, hogy a követelmények megsértése esetén képes végrehajtási szekvenciával (ellenpéldával) demonstrálni a rendszer helytelen működését. Állapotelérhetőség vizsgálatakor kiemelten fontos az elérhető állapotokba vezető szekvenciák generálása, mivel sok alkalmazási területen (például modellalapú tesztelés) a fő kimenet maga az ellenpélda.

Az első modellellenőrzők a problémát a rendszer lehetséges állapotainak szisztematikus és gyakran kimerítő átvizsgálásával, vagyis az állapottér gráfjának előállításával oldották meg. Ezeket az algoritmusokat explicit modellellenőrzőknek nevezzük, mivel az állapotokat és állapotátmeneteket explicit módon tartják nyilván. Ez a megoldás azonban nagyon hamar korlátokba ütközik, mivel az állapottér már viszonylag kis modellek esetén is kezelhetetlenül nagyméretű lehet: ezt a jelenséget a szakirodalom állapottér-robbanásnak nevezi.

Az állapottér-robbanás kezelésének egyik, a dolgozatban is használt módja a szimbolikus modellellenőrzés, amely az állapotok belső szerkezetét kihasználva döntési diagramokként kódolja el az állapotteret. Ezzel jelentősen növeli a kezelhető állapottér méretét, ugyanakkor megnehezíti az explicit modellellenőrzőkben alkalmazott technikák használatát és az ellenpéldák generálását is.

Konkurens rendszerekben az állapottér-robbanásnak gyakori oka az egymástól független aszinkron műveletek teljes sorrendezése, amely rengeteg, a követelmény szempontjából érdektelen köztes állapothoz vezet. A részleges rendezéses redukció az ekvivalens sorrendezéseket egyetlen reprezentatív szekvenciával helyettesítve csökkenti a bejárt állapotok számát. A módszer az explicit modellellenőrzésre épít, így az ott használt technikák többnyire alkalmazhatóak maradnak.

Ebben a dolgozatban két, egymást kiegészítő algoritmust adunk az elérhetőségi probléma és az ellenpéldagenerálás megoldására. Első lépésként egy szimbolikus algoritmus megállapítja, hogy a célállapotok elérhetőek-e, majd az elérhető állapotokról szerzett információt átadja egy explicit, vezérelt modellellenőrző algoritmusnak, amely így képes az elérhető állapotokba vezető végrehajtási szekvenciák hatékony előállítására. Az eredményként kapott hibrid modellellenőrző algoritmus 1) a szimbolikus kódoláshoz az ún. hierarchikus döntési diagramokat használja, 2) az explicit módon felderítendő állapotteret a részleges rendezéses redukció használatával hatékonyan csökkenti, illetve 3) az explicit keresést vezérelt módon, a modell és a követelmények struktúráját figyelembe véve hajtja végre. A két algoritmus között átadott adatok lehetővé teszik, hogy a szimbolikus és explicit módszerek gyengeségeit a másik módszer erősségeivel kompenzáljuk.

szerzők

• 
  Élő Dániel
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)
• 
  Soltész Adrián
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)

konzulensek

• 
  Dr. Molnár Vince
  Adjunktus, Méréstechnika és Információs Rendszerek Tanszék
• 
  Dr. Vörös András
  egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék

helyezés