22 Jun 2020 - Dan Kristiansen
Jeg er færdiguddannet fra Aalborg Universitet med den højest mulige karakter. Censor gav meget positiv feedback om selve afhandlingen med plads til forbedringer med hensyn til præsentationen.
Min afhandling demonstrerer en tilgang til korteste sporbarhedbarhedsanalyse af vægtede pushdown-systemer. De vægtede Pushdown-systemer bruges til at modellere MPLS-netværk (Multiprotocol Label Switching) i AalWiNes. Vi analyserer især MPLS-netværk. MPLS er en netværk routing teknik, der bruger korte stikketiketter til at rute trafik snarere end lange netværksadresser. Dette undgår komplekse opslag i rutetabeller, hvilket gør netværkstrafikken mere fleksibel og hurtigere. MPLS bruges til at oprette hurtigt WAN (wide wide area network) og virtuelle private netværk (VPN) og kan bruges af netværksudbydere til hurtigt at tunnelere IP-trafik gennem deres undernetværk. Værktøjet giver mulighed for at analysere netværket under flere fejl, hvor en etiket skubbes oven på de eksisterende etiketter og bruges til at rute pakken via en alternativ sti. Når pakken kommer tilbage på den oprindelige sti, dukker den ekstra etiket op.
De vigtigste bidrag i denne afhandling er anført og forklaret nedenfor:
Vi introducerede rækkevidde biblioteket (1) som en forbedring af ydeevnen for AalWiNes, som tidligere brugte værktøjet Moped til at udføre uvægtet ikke-deterministisk PDA rækkevidde analyse og sporgenerering. Implementeringen af biblioteket PDAAAL tillader, at tilgængelighedsanalysen kan være en integreret del af værktøjet snarere end en ekstern Moped-binær, der introducerer ydelsesomkostninger ved parsning. Den vægtede udvidelse (2) modellerer pushdown-systemer med vægte, hvilket giver mulighed for korteste sporspørgsmål ved hjælp af en kombination af forskellige kvantitative egenskaber ved netværkssporene som vægte. Forespørgsler kan annoteres for at minimere disse egenskaber, de understøttede egenskaber, der skal minimeres i sporet, er: antal humle, antal fejl, antal tunneler og den fysiske afstand. Et ikke-trivielt problem er at minimere den globale egenskab for den maksimale stabelstørrelse under et spor (3).
Den tidlige termineringskontrol (4) introduceres som en forbedring af ydeevnen i algoritmerne til rækkevidde af PDAAAL. Den tidlige termineringskontrol implementeres som en konstant tidsopslag i det nuværende system og afsluttes, hvis måltilstanden allerede er nået, snarere end at opbygge det komplette sæt tilgængelige stater. Netværksmanipulation (5) er et bidrag til den eksisterende AalWiNes-implementering, så vi kan skabe store, realistiske netværkstopologier til test. Manipulationen fungerer som en algebra til at kombinere netværkstopologier med sammenkædning og injektion. Routinggenerering (6) opretter for enhver netværkstopologi en routingtabel, således at der findes etiketskiftede stier mellem alle par routere og hurtige omdirigeringstier til alle kanter. Hvis nogen kant i netværket mislykkes, anvendes en sådan hurtig omdirigeringssti i stedet for den svigtende kant. En anden ydelsesforbedring introduceres ved at reducere operationssekvensen (7). Et sæt af driftssekvensreduktionsregler er defineret, således at operationssekvenser reduceres til mindre sekvenser med samme opførsel.
Endelig foretager vi en eksperimentel evaluering for at sammenligne effektiviteten af vores implementering med Moped. Netværkene, der blev brugt i dette eksperiment, er konstrueret ud fra fem forskellige netværkstopologier fra Topology Zoo, som hver er manipuleret til seks forskellige størrelser og annoteret med genererede routingtabeller. Eksperimentet udføres i en klynge leveret af Aalborg Universitet og inkluderer 200 tilfælde af forespørgsler for hvert af de 30 forskellige netværk. Ydelseseksperimenterne fanger bekræftelsestidspunktet for Moped og PDAAAL og sammenligner dem direkte i hvert testtilfælde. Fra eksperimentet kan vi konkludere, at PDAAAL er bedre end det avancerede værktøj Moped. Et andet eksperiment inkluderer den vægtede udvidelse til PDAAAL og fanger resultaterne af at verificere de samme førnævnte netværk og forespørgsler. Resultaterne viser forbedringerne ved at kommentere systemet med vægte, f.eks. for at minimere antallet af links i sporet, således at den vægtede udvidelse forbedrer sandsynligheden for, at der findes en gyldig spor, mens der kun er lidt ydelsesomkostning for den vægtede rækkevidde-algoritme.
