Konkurens programok HW-SW együttes verifikációja

A folyamatosan fejlődő technika világában egyre több olyan szituáció fordul elő, ahol sok ember élete múlik számítógépek helyes működésén - legyen szó akár egy önvezető autóról, repülőről vagy atomreaktorok biztonsági rendszeréről. A legfontosabb elvárás az ilyen rendszerekkel szemben az, hogy lehetőleg elkerüljék a kritikus hibákat. Tekintve, hogy számos alkalommal történt már emberéleteket követelő katasztrófa rosszul működő programok vagy számítógépek miatt, elfogadhatjuk, hogy az ilyen rendszerek működésének alapos ellenőrzése különösen indokolt éles használat előtt - az ellenőrzés egy precíz módja az, hogy matematikailag bizonyítjuk, hogy a rendszer előre látható működése során nem történhet hiba.

Szoftverek ellenőrzésére számos sikeres keretrendszer létezik, amelyek a programokat formális modellként ábrázolva képesek bizonyos követelmények teljesülését vizsgálni. Azonban a teljes rendszer verifikációjával kevesen próbálkoztak, pedig hiába tökéletes a szoftver, ha egy hardveres hiba képes akár az egész rendszert térdre kényszeríteni. A hardver és szoftver együttes verifikációja még nehezebb több processzormagos környezetekre. Ennek a kutatásnak a fő célja a többmagos eszközök és a rajtuk futó konkurens programok együttes ellenőrzése. Egy olyan megközelítést fejlesztettem ki, ami nem csak a konkurens programok verifikációjával foglalkozik, de a többmagos rendszereken futó magasszintű nyelvek memóriamodelljének (MCM) megsértését is vizsgálja. A témám alapja egy korábbi kutatás, ahol a szerzők megmutatták, hogy sok, potenciálisan hibát okozó inkonzisztencia fordul elő a modern architektúrákon.

Ezen projekt keretein belül egy olyan megközelítést mutatok be, ami az ilyen biztonságkritikus rendszereket fejlesztő programozókat segíthet a formális verifikáció és MCM validáció eszközeinek segítségével, ezzel biztonságosabb, megbízhatóbb kódot eredményezve. Továbbá bemutatok egy prototípus implementációt ami ezen munkafolyamat több lépését automatizálja, ezzel a következő funckionalitást biztosítva:

• Egy {mikroarchitektúra, ISA, magasszintű nyelv} kombináció automatikus verifikációja, felderítve az MCM-et sértő szituációkat.

• C11 kód formális modellbe való átalakítása, ezzel lehetővé téve a formális verifikációs eszközök használatát.

• Automatikus lekérdezés generálás a fent említett verifikációs eszközök használatához.

• Visszajelzés a potenciálisan hibát okozó kódsorokról.

• Mitigáció automatikus ajánlása mutex zárak és feltételes szinkronizáció használatával.

szerző

• 
  Bajczi Levente
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)
  

konzulensek

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

helyezés