Formális verifikációval támogatott tesztgenerálás autóipari környezetben
Szoftverek egyre több kritikus feladatot látnak el biztonságkritikus rendszerekben, mint például autókban, repülőgépekben vagy erőművekben. Sokszor korábbi mechanikus/hidraulikus megoldásokat is beágyazott szoftverrel váltanak ki vagy szoftverrel támogatnak meg, például egy autó kormányművében.
Ezek a beágyazott szoftverek egyrészt kritikusak a rendszer működése szempontjából, másrészt viszont egyre összetettebbek is. Emiatt különösen fontos olyan módszereket használni, amelyek képesek ezen beágyazott szoftverek hibáit megtalálni vagy a helyességüket bizonyítani. A tesztelés hatékonyan, alacsony számítási igény mellett képes hibákat találni a meglévő rendszerekben, valamint a biztonságkritikus-rendszerek fejlesztését szabályozó szabványok alapvető elvárásként tekintenek az mélyretekintő, alaposan dokumentált tesztelésre. Azonban a tesztelés önmagában a helyesség bizonyítására nem alkalmas. Ezzel szemben a formális verifikáció a szoftver matematikai modelljét vizsgálja és matematikailag bizonyítja a különböző hibák elő nem fordulását. A formális verifikáció egy számításigényes feladat, hiszen az algoritmusnak meg kell vizsgálnia a program összes lehetséges viselkedését és állapotát, és még a legegyszerűbb programoknak is könnyen lehet végtelen nagyságú állapottere. Az elmúlt két évtizedben számos áttörést sikerült elérni a formális verifikáció területén, azonban a probléma nehézsége miatt sok esetben nem nyújtanak megoldást.
A munkám célja, hogy ezt a két különböző megközelítést alkalmazzam kombinálva autóiparban használt AUTOSAR környezetben, ötvözve a két módszer előnyeit. Munkám során kidolgozok egy olyan algoritmust, amely a verifikáció eredményeit kihasználja a teszgenerálás során, továbbá kihasználom az AUTOSAR szoftverkomponensek sajátosságait. Sikeres verifikáció esetén a vizsgált komponens helyessége eldöntött, és vagy egy bizonyítás áll rendelkezésre igazolva a helyességet, vagy egy olyan ellenpélda, aminek segítségével a hiba reprodukálható. Amennyiben a verifikáció sikertelen, teszteket generálok, felhasználva a formális verifikáció során a bejárt állapottérből kinyert információt. Ennek kapcsán több különböző tesztgenerálási stratégiát is kifejlesztettem, amelyek különböző típusú hibák megtalálására hatékonyak.A megközelítésemet egy autóipari példán is megvizsgálom és bemutatom a hatékonyságát.
szerző
-
Dobos-Kovács Mihály
Villamosmérnöki szak, alapképzés
alapképzés (BA/BSc)
konzulens
-
Dr. Vörös András
egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék