9.4.2020

Doktorsavhandling i datavetenskap

MSc Muhammad Usman Sanwals doktorsavhandling i datavetenskap framläggs till offentlig granskning fredag 17.4.2020 vid fakulteten för naturvetenskaper och teknik vid Åbo Akademi.

Avhandlingen heter Formal Model Refinement for Complex Biological Systems.

Det finns ett stort intresse för att konstruera omfattande biologiska modeller. Olika metoder används för att bygga upp dessa modeller. Mera omfattande modeller behövs för att kunna beskriva ett systems globala beteende, som är ett resultat av en mängd interaktioner mellan lokala processer. Speciellt inom områden där man ser på helheter för olika system, till exempel inom systembiologin, systemmedicinen, systemimmunologin, etc.

Vanligtvis har mera omfattande modeller skapats genom en sammanslagning av flera existerande delmodeller och mera detalj har sedan lagts till i den slutliga modellen. Sådana modeller är sällan lyckade inom biologin, medan inom utvecklingen av mjukvarusystem är denna metod ett vanligt tillvägagångssätt. Huvudorsaken till detta är att interaktionerna mellan delmodellerna inte tas i beaktande i sammanslagningen så den slutliga modellen förblir i stora drag endast en samling separata modeller. Följaktligen uppvisar den nya modellen undermålig passning till laboratoriedata då den används, detta även om modellerna separat för sig var passade till deras data. Som en följd av detta måste modellpassningen göras om antingen helt eller delvis, en process vars svårighet med avseende på komplexiteten ökar snabbt relativt till modellens storlek. För att detta ska lyckas krävs det även mer och mer data.

Det tillvägagångssätt vi valde i denna avhandling var att stegvis utveckla en komplex modell, utgående från en basmodell. Vid varje tillägg till basmodellen försäkrade vi oss om att de kvantitativa egenskaperna för modellen bibehölls, såsom modellens anpassningsförmåga till data. Vi använde oss av Event-B modellering för att åstadkomma detta. Event-B har många fina egenskaper för modellförfining, vilket är viktigt vid omfattande modellutveckling. I Event-B byggs omfattande modeller upp genom stegvis förfining.

Vi börjar med en basmodell vilken endast har begränsade detaljer och utökar modellen med ny information genom olika förfiningssteg. Modellerna vi får av förfiningen genom Event-B är formellt relaterade till varandra genom en förfiningsrelation och kan användas på vilken detaljnivå som helst. Event-B stöder verktyget Rodin, vilket används som verktyg för formell verifiering vid varje steg av modellutvecklingen. Så vitt vi vet är detta första gången som Event-B har använts för att modellera biologiska system.

Muhammad Usman Sanwal disputerar fredagen den 17 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/616584778. (Se nedan för praktiska anvisningar.) Opponent är Dr. David Šafránek, Masaryk University, Tjeckien, och kustos är docent Luigia Petre, Åbo Akademi.

Muhammad Usman Sanwal är född 5.1.1985 i Vehari, Pakistan. Han avlade MSc-examen 2012 vid National University of Sciences & Technology (NUST), Islamabad, Pakistan.

Muhammad Usman Sanwal kan vid behov nås per telefon 046 520 9777 eller e-post muhammad.sanwal@abo.fi.

Avhandlingen finns elektroniskt i Doria: https://www.doria.fi/handle/10024/176640?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. Du behöver inte skapa ett Zoom-konto eller logga in någonstans för att kunna följa med disputationen. Om du installerar appen deltar du genom att klicka på möteslänken varefter du börtillåta att länken öppnas i Zoom-appen.

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.