Lineáris tranzíciós rendszerek absztrakt interpretáció alapú verifikációja

A lineáris tranzíciós rendszerek (LTR), mint például a Petri-hálók, többek között az aszinkron, elosztott, konkurens, párhuzamos és nem-determinisztikus rendszerek elterjedt grafikus és matematikai modellező eszközei. A LTR modellek viselkedését az állapottér, azaz az elérhető állapotok és az állapotátmenetek halmaza adja meg.
A formális verifikáció egyik legfontosabb vizsgálata az ún. elérhetőségi analízis, amely azt vizsgálja, hogy egy adott állapot elérhető-e engedélyezett állapotátmenetek sorozatával egy adott kezdőállapotból kiindulva. Ezen eldönthetőségi probléma a matematika nehéz problémái közé esik, ezért hatékony algoritmusokra van szükség.
Az irodalomban ismert egyik hatékony algoritmus az absztrakt interpretáció, amely az állapottér egy véges, absztrakt reprezentációján végez következtetéseket.
A hallgató feladata megvizsgálni az absztrakt interpretáció algoritmusát, és amennyiben lehetséges, továbbfejleszteni azt a tanszéki fejlesztésű modellellenőrző keretrendszerben.
A hallgató feladatának a következőkre kell kiterjednie:

  • Mutassa be az absztrakt interpretáció algoritmusát.
  • Tervezzen meg egy absztrakt interpretációt használó verifikációs modult a tanszéki fejlesztésű modellellenőrző keretrenszerbe.
  • Implementálja az algoritmust.
  • Vizsgálja meg az algoritmus továbbfejlesztési lehetőségeit.
Jelleg: 
Elméleti és gyakorlati
Konzulens: 
Vörös András
TDK lehetőség: 
TDK lehetőség
Megismerhető technológiák: 
Eclipse, Java, algoritmusok
Állapot: 
Folyamatban