Modellalapú automatatanulás formális modellek szintéziséhez

Összetett kiberfizikai rendszerek tervezésére széles körben alkalmaznak modellvezérelt tervezést, amely fejlett modellező nyelvek bevezetésével megkönnyíti a rendszerek megvalósítását. A modellek alkalmasak formális módszerekkel való ellenőrzésre, ami biztonságkritikus feladatkörben - például okos járművek esetében - kiemelten fontos. Továbbá automatikus kódgenerátorok alkalmazásával a rendszer legfőbb komponensei automatikusan előállíthatóak, beleértve a komponensek helyes viselkedéséért felelős monitorozást is.

Azonban számos szoftverkomponensnek – különös tekintettel a korábban vagy külső felek által fejlesztetteknek – nem áll rendelkezésre megfelelően precíz modellje, ami megakadályozza a formális módszerek alkalmazását. Továbbá az elvárt viselkedés specifikációjának hiányában a monitor komponensek sem képesek detektálni az esetleges hibákat. Különösképpen az időzített komponensek viselkedését nehéz formalizálni.

Dolgozatunk célja, egy olyan specializált algoritmus kidolgozása, mely megfigyelve egy időzített rendszer viselkedését, a megfigyelt események alapján képes formális modelleket szintetizálni. A tanulás támogatására az irodalomból ismert korszerű automatatanuló algoritmusokra támaszkodunk. Célunk ezen algoritmusok kiterjesztése a mérnöki tervezésben gyakran alkalmazott absztrakció hatékony kezelésével, ezáltal lehetővé téve a fókuszált tanulást.

Megközelítésünk újszerűségét a modellalapú bemeneti nyelv és ennek az időzített automata tanuló algoritmusokkal való kombinációja adja. Munkánk során elkészítettünk egy modellalapú automatatanuló keretrendszert időzített szoftverkomponensek mérnöki modelljének szintetizálására. Gráfmintaillesztő nyelvet használunk a tanulás fókuszálására, azaz az absztrakció definiálására. A definiált absztrakció alapján az automatatanuló algoritmus előállítja a rendszer időzített formális modelljét. Az elkészült szoftver felhasználását esettanulmányokkal demonstráljuk.

Módszerünk által lehetővé válik olyan szoftverkomponensek viselkedésének megtanulása, amelyekre eddigiekben nem volt lehetőség komplexitásuk, illetve időtől függő viselkedésük miatt. Az így létrejövő specifikációból a komponens viselkedését formálisan ellenőrizhetjük, anomáliadetektáló monitort származtathatunk, valamint dokumentációt, illetve teszteket generálhatunk.

szerzők

• 
  Gujgiczer Anna
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)
• 
  Elekes Márton
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)

konzulensek

• 
  Farkas Rebeka
  doktorandusz, Méréstechnika és Információs Rendszerek Tanszék
• 
  Tóth Tamás
  tudományos segédmunkatárs, 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