26.3.2020
Doktorsavhandling i datateknik/programvaruproduktion
MSc Faezeh Siavashis doktorsavhandling i datateknik/programvaruproduktion framläggs till offentlig granskning torsdag 2.4.2020 vid fakulteten för naturvetenskaper och teknik vid Åbo Akademi.
Avhandlingen heter Model-based Verification and Testing of Web services – Functionality, Robustness and Vulnerability Analysis.
Webbtjänster är mjukvarusystem som är designade för att stöda växelverkan mellan maskiner över ett nätverk. Dessa tjänster ger tillgång till ett brett utbud resurser från persondatorer och mobiltelefoner. I dagens läge kan man se en förbättring av traditionell affärsverksamhet och manuella tjänster tack vare av webbtjänster.
Användare av webbtjänster förväntar sig inte bara att de är kontinuerligt tillgängliga, men att de också uppfyller alla krav på datasäkerhet. Dock finns det många orsaker som gör att det inte är lätt att säkerställa kvaliteten av webbtjänsters implementationer. För det första är de tillgängliga för ett stort antal användare globalt, genom allmänna kommunikationsprotokoll. Därför borde webbtjänster vara tillräckligt robusta för att kunna acceptera en korrekt inmatning men också rata en inkorrekt eller skadlig inmatning. För det andra hänger webbtjänsters anseende på hur de förväntas prestera på samma gång som de måste bevara integriteten för alla användares data. Den tredje orsaken är att webbtjänst-implementationer borde utvecklas så att de kan garantera att den implementerade åtkomstkontrollen är verksam. När man utvecklar ny funktionalitet och förändrar existerade funktionaliteter krävs att man uppmärksammar att det inte sker oavsiktliga förändringar i åtkomstkontrollen.
Mjukvarutestning är en av metoderna som används för säkerställning av kvaliteten för mjukvarusystem. Mjukvarutestning går ut på att man gör en inmatning till systemet under testning och utmatningen från systemet jämförs med en förväntad utmatning. Mjukvarutestning är vanligen en informell process som ofta lämnas kvar till slutet av utvecklingsprocessen, så att den ofta minskas i omfång för att passa projektets deadline. Därför finns det ett behov av att använda sig av nya mjukvarutestningsmetoder så att testningen blir både effektiv och verksam.
I denna avhandling definierar vi ett tillvägagångssätt för modellbaserad testning för att utvärdera beteendet av webbtjänster och kombinationer av webbtjänster. Målet med att skapa modeller är att man ska kunna göra en verifierbar specifikation av webbtjänsten, som man senare ska kunna använda för att generera mjukvarutest som jämförs mot implementeringen av webbtjänsten. I vårt tillvägagångssätt använder vi en modelchecking-metodik för att säkerställa att webbtjänstens krav möter den modellbaserade specifikationen. Efter detta använder vi modellbaserad mjukvarutestning för att säkerställa att implementeringen av webbtjänsten motsvarar den verifierade specifikationen och som konsekvens också webbtjänstens krav.
Först studerar vi hur samverkan mellan webbtjänster och dess omgivning kan modelleras och hur den kan användas för generering av mjukvarutest. För detta ändamål gjorde vi en systematisk litteraturstudie om hur andra har använt modeller av omgivningen i modellbaserad mjukvarutestning. Efter detta presenterar vi ett tillvägagångssätt där webbtjänstens omgivning modelleras med ett UML-sekvensdiagram, medan webbtjänsten själv beskrivs med UML-tillståndsmaskiner. Båda modeller översätts till UPPAAL timed automata för att man ska kunna verifiera att tjänsternas beteenden tillåter specificerad samverkan. Därtill verifierar vi att webbtjänstens olika krav uppfylls. Den verifierade resulterande modellen används för online generering av mjukvarutest mot en implementering av webbtjänsten.
Som ett andra bidrag i denna avhandling, definierar vi ett tillvägagångssätt för att utvärdera webbtjänsters robusthet och säkerhets sårbarheter i närvaro av oförväntade och ogiltiga tillstånd och inmatningar. För detta utökar vi vårt modellbaserade tillvägagångssätt i avseende på mutationstestning. I modellbaserad mutationstestning modifieras det ursprungliga testet med en muteringsoperator för att skapa ett aningen inkorrekt beteende. Mutantmodeller används för att generera mjukvarutest som ger inkorrekta inmatningar, så att robustheten mot sådana inmatningar kan utvärderas, på samma gång som nya säkerhetsbrister kan uppdagas.
Slutligen breddar vi det ovanstående tillvägagångssättet med två bidrag. Först definierar vi en samling muteringsoperatorer för UPPAAL timed automata som vi utvärderar empiriskt inom sammanhanget för webbtjänster. Sedan presenterar vi en ny metod för att välja ut muteringar som kan utesluta mutationer som inte är användbara i testningssyfte. Genom att använda denna metod kan man minska mjukvarutestens tidsanspråk. Våra resultat visar att dessa metoder förbättrar vårt tillvägagångssätts effektivitet och gör det mera verksamt.
Under arbetet för denna avhandling har flera verktyg använts som stöder den presenterade mjukvarutestningsmetodiken. I några studier använde vi verktyg som UPPAAL model checker och UPPAAL TRON test generator. I andra fall har vi kompletterat existerande verktyg. Ett exempel på ett verktyg som vi implementerade är MuUTA som automatiserar mutantgenerering, urval av mutanter och en mutantexekveringsprocess.
Tillvägagångssätten som definieras i denna avhandling har tillämpats i två fallstudier. Våra resultat visar att vår mjukvarutestningsmetodik kan göra omfattande utforskning av ett systems beteende, så att nya fel som annars skulle förbli oupptäckta av traditionella modellbaserade metoder kan bli avslöjade.
Faezeh Siavashi disputerar vid Åbo Akademi torsdagen den 2 april 2020 kl. 13. På grund av rådande omständigheter kan disputationen inte följas på plats och ställe, utan på distans via adressen: https://aboakademi.zoom.us/j/387656692. (Se nedan för praktiska anvisningar.) Opponent är associate professor Cristina Seceleanu, Mälardalens högskola, Sverige, och kustos är docent Dragos Truscan, Åbo Akademi.
Faezeh Siavashi är född 21.9.1982 i Babol, Iran. Hon avlade BSc-examen 2006 vid Azad Teheran University, Iran, och MSc-examen 2012 vid Åbo Akademi.
Faezeh Siavashi kan vid behov nås per telefon 040 444 5565 eller e-post fasiava@gmail.com.
Avhandlingen finns elektroniskt i Doria: https://www.doria.fi/handle/10024/176843?locale=lsv.
Klicka på bilden för att få fram en tryckduglig version.
Bilden får fritt användas av medierna.
Praktiska anvisningar för att följa med disputationen på distans
För att följa med disputationen behövs programvaran Zoom eller webbläsaren Google Chrome.
Under disputationen bör åhörarna inte slå på sin mikrofon eller video (av sig själva).
I slutet av tillställningen är det möjligt att ställa frågor. Har du en fråga kan du visa det genom funktionen ”Raise Hand”. Förbered dig gärna genom att ha en mikrofon installerad på din dator eller genom att ha frågan färdigt formulerad i ett textdokument på datorn därifrån du sedan kopierar in den i Zooms chattfunktion. Frågor om åhörarnas ev. tekniska problem bör inte ställas via Zooms chatt.