témavezető: Kovásznai Gergely
helyszín (magyar oldal): Debreceni Egyetem Informatikai Kar helyszín rövidítés: DE IK
A kutatási téma leírása:
Vezetéknélküli szenzorhálózatokat (Wireless Sensor Network = WSN) napjainkban az ipar, a mezőgazdaság, az intelligens közlekedés, a hadászat és – úgy általában – az élet legkülönfélébb területein használnak. A hálózatokat felépítő szenzoregységek akkumulátorai véges kapacitásúak, ezért a hálózatok üzemeltetésének energiahatékonysága elsődleges prioritás. Legalább ilyen fontos a hálózatok biztonságos üzemeltetése, különös tekintettel a kritikus rendszerekben üzemeltetett hálózatokra.
A formális módszerek segítségével képesek vagyunk olyan rendszerek verifikációját is megvalósítani, melyek esetén a kimerítő tesztelés nem megoldható és/vagy nem nyújt megfelelő garanciát. Egy nagy potenciállal rendelkező irány a SAT és SMT szolverek alkalmazása, melyeket manapság már széles körben használnak az iparban komplex rendszerek (pl. hardver, szoftver, repülésirányító rendszerek stb.) formális verifikációjára. Míg a verifikáció azt garantálja, hogy létezik a WSN-ünk üzemeltetésének egy biztonságos modellje, addig az optimalizáció egy olyan optimális modellt garantál, mely mellett a WSN a lehető legtovább üzemképes; ennek vizsgálatára – például – MaxSAT és OMT szolvereket használhatunk.
A téma keretében meglévő kutatásba lehet becsatlakozni, már meglévő eredményekkel. Megalkottuk a WSN-eknek egy formális modelljét, mely magában foglalja a gyakorlatban fontos biztonsági kritériumokat is. Sikeresen verifikáltunk és optimalizáltunk WSN-eket meglévő OMT szolverek segítségével (Z3, OptiMathSAT, Symba). Saját OMT szolvert fejlesztettünk (Puli 2.0), mely jóval hatékonyabbnak bizonyult a meglévő szolvereknél a WSN és egyéb optimalizációs problémákat reprezentáló benchmarkokon. A kutatás folytatódik a saját OMT szolverünk továbbfejlesztésével, újabb megoldó algoritmusok implementálásával, valamint a formális WSN modellünk kiegészítésével oly módon, hogy az az energiahatékonyság minél több fizikai paraméterét vegye figyelembe.
Irodalom
• G. Kovásznai, Cs. Biró, B. Erdélyi. Puli – A Problem-Specific OMT solver. 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), aff. to IJCAR 2018, 2018.
• G. Kovásznai, Cs. Biró, B. Erdélyi. Generating Optimal Scheduling for Wireless Sensor Networks by Using Optimization Modulo Theories Solvers. 15th International Workshop on Satisfiability Modulo Theories (SMT 2017), aff. to CAV 2017, CEUR, Vol. 1889, pp. 15-27, 2017.
• Q. Duan, S. Al-Haj, E. Al-Shaer. Provable configuration planning for wireless sensor networks. 8th Int. Conf. on Network and Service Management (CNSM) and Workshop on Systems Virtualization Management (SVM), pp. 316–321, 2012.
• R. Sebastiani, P. Trentin. OptiMathSAT: A tool for optimization modulo theories. Int. Conf. on Computer-Aided Verification (CAV), LNCS, vol. 9206, pp 447-454.
Jelentkezési határidő: 2021-11-15
2024. IV. 17. ODT ülés Az ODT következő ülésére 2024. június 14-én, pénteken 10.00 órakor kerül sor a Semmelweis Egyetem Szenátusi termében (Bp. Üllői út 26. I. emelet).
Bejelentkezés
