Formal Methods for Modelling Wireless Sensor Networks

Abstract

Ebben a disszertációban olyan új formális módszereket mutattunk be, amelyek alkalmasak vezeték nélküli szenzorhálózatok modellezésére és működésük elemzésére. Az értekezés eredményeit hazai és nemzetközi konferenciákon, valamint folyóiratokban publikáltuk. A bevezetésben ismertettük a szerző által elért eredményeket, majd a második fejezetben áttekintést adtunk a kutatási területről, a téma elméleti hátteréről és a kapcsolódómunkákról. Az I. fejezetben két nulladrendű logikai modellt mutattunk be. Egyrészt ismertettünk egy olyan algoritmust (WnDGen), amellyel nehéz kombinatorikai benchmark-ok generálhatók, másrészt definiáltunk egy irányított gráfok reprezentálására alkalmas formulát (Black-and- White 2-SAT). Ezek után ismertetésre került két új szekvenciális SAT szolver (CSFLOC, BaW 1.0), valamint megmutattuk, hogy ezek hogyan használhatók WSN alapú problémák megoldására. Ugyancsak ebben a fejezetben került bemutatásra, hogy hogyan oldhatók meg propozicionális kielégíthetőségi problémák elosztott számítási erőforrások használatával. A harmadik fejezetben egy véletlenszerűen telepített és heterogén csomópontokból álló vezeték nélküli szenzorhálózat leírására alkalmas, rádió energia modellen alapuló, hálózat élettartamára optimalizálható SMT alapú reprezentációt ismertettünk. Definiáltunk egy új modell alapú inkrementális optimalizálási eljárást. A fejezet végén bemutattunk egy probléma specifikus OMT solver-t, a Puli-t. A negyedik fejezetben bemutatásra került három új sűrűség és három új redundancia alapú lokális metrika (WCGD, RCGD, WRCGD, CGR, WCGR-klikk érték és méret alapú), melyeket összehasonlítottuk a szakirodalomból eddig ismert metrikákkal, és bemutattuk, hogyan használhatók csomópontok rangsorolására, továbbá klasszifikálásra. A dolgozat elején három tézist fogalmaztunk meg. A tézisekhez köthető eredményeket rendre a 3.3 és a 3.4 (I. tézis), az 5.3 és az 5.4 (II. Tézis) valamint a 6.3, a 6.4, és a 6.5 (III. Tézis) fejezetek voltak hivatottak bemutatni.