A modern autók gyártását igen alapos tervezési folyamat előzi meg. Ennek során a rendszermérnökök összegyűjtik, hogy milyen funkciókra van szükség egy adott autótípusban (legyen-e benne ABS, kipörgésgátló, tempomat/adaptív sebességszabályozó stb.), és az egyes funkciók között milyen kapcsolatoknak kell lenniük (pl. a fékpedál lenyomásakor az ABS bekapcsol, a tempomat viszont kikapcsol) – ez utóbbiakat nevezik tervezési kényszereknek.

A tervezés során a mérnökök (szoftveralapú) tervezőeszközöket használnak, amelyekkel az autónak különböző modelljeit készítik el. A modellek használatának az a célja, hogy az autó tényleges legyártása nélkül is meg lehessen vizsgálni bizonyos funkciókat. Így például lehet virtuális töréstesztet végezni anélkül, hogy egy autót összetörnének, és egy tempomat vezérlőszoftvere is tesztelhető anélkül, hogy fizikailag is rászerelnék a kormánykerékre. A modellek használata arra a feltételezésre épít, hogy ha gond van a modellen, akkor gond lehet az éles rendszerben is, illetve, ha a modell betartja a különféle tervezési kényszereket (vagyis „jól formált”, ahogy a rendszermérnökök mondják), akkor az éles rendszer is jól viselkedik majd.

Hibakeresés gráfmodellekkel

Persze a tervezőeszközök is csak szoftverek – azaz elvileg ugyanúgy lehetnek bennük szoftverhibák, mint egy egyszerű mobilalkalmazásban –, tehát magát a tervezőeszközt is nagyon alaposan le kell tesztelni. Ez a szisztematikus tesztelés (amely a tanúsítványozási folyamat része) igen bonyolult és költséges folyamat, de feltétlenül szükség van rá ahhoz, hogy az autógyártó cég megbízhasson a modellek használhatóságában.

A valódi autók egyes funkcióinak pontos kapcsolati hálózata (gráfmodellje) csupán a tervezési lehetőségek egy töredékét használja fel, ezért a tervezőeszközök tesztelésére nem alkalmas. Helyette olyan tesztmodelleket kell előállítani, amelyekkel a tervezőeszközök alapos tesztelése elvégezhető úgy, hogy azok felépítésüket és méretüket tekintve hasonlítsanak a valóságban használatos modellekre. A tervezési kényszerek – melyekből egy modern autó esetében 500-nál is több lehet – azonban ismertek, és ha a tervezőrendszer az ilyen kényszereknek megfelelő (vagyis jól formált) gráfmodellekkel általában hibátlanul működik, akkor a valódi autó funkcióinak kapcsolatait is jól kezeli majd.

Az efféle jól formált gráfmodellek előállítása matematikailag nehéz probléma. A jelenlegi módszerek legtöbbször ún. automatikus tételbizonyító eszközökön alapulnak, amelyek logikai formulák kielégíthetőségére vagy egy tétel axiómákból való levezethetőségére vezetik vissza a problémát. Ezek a logikai megoldók jól formált gráfmodellek generálásakor mindössze 100-150 csomópontból álló gráfot képesek előállítani, ami sokkal kisebb, mint az éles ipari alkalmazásokhoz szükséges modellméret.

Az MTA-BME Lendület Kiberfizikai Rendszerek Kutatócsoport munkatársai, Semeráth Oszkár, Nagy András Szabolcs és a kutatócsoport vezetője, Varró Dániel olyan szoftverprototípust fejlesztett ki a nyílt forráskódú VIATRA keretrendszerre építve, amely különféle gráfalgoritmusok és módszerek felhasználásával képes jól formált gráfmodelleket automatikusan előállítani. Az így előállított gráfok sokkal nagyobbak (akár 5-7 ezer csomópontjuk is lehet), további kapcsolódó kutatásaik pedig azt is kimutatták, hogy az így kapott modellek valósághűbbek is, mint a logikai megoldók által előállított gráfok. Eredményeiket tavasszal mutatják be a szakma legrangosabb konferenciáján, az ICSE-n.

Hosszú távon a keretrendszer elősegítheti a biztonságkritikus rendszerek (autók, repülőgépek, egészségügyi berendezések stb.) tervezése során használt egyes tervezőeszközök szisztematikus ellenőrzését, de a módszer felhasználható lehet autonóm és intelligens vezérlők (pl. önjáró autók, drónok) automatikus tesztelésére is. Az eredmények ipari kiértékelését már meg is kezdte a Lendület-kutatócsoporthoz több szállal is kötődő innovatív magyar vállalkozás, az IncQuery Labs Kft, amelynek alapítói között ott találjuk Varró Dánielt és több korábbi PhD-hallgatóját.