9.4.2020
Tohtorinväitös tietojenkäsittelytieteen alalta
MSc Muhammad Usman Sanwalin väitöskirja tietojenkäsittelytieteen alalta esitetään julkisesti tarkastettavaksi Åbo Akademin luonnontieteiden ja tekniikan tiedekunnassa perjantaina 17.4.2020.
Väitöskirjan otsikkona on Formal Model Refinement for Complex Biological Systems.
Laajojen biologisten mallien rakentaminen on herättänyt suurta kiinnostusta ja synnyttänyt erilaisia lähestymistapoja. Kokonaisvaltaisempia malleja tarvitaan systeemitason simuloinnissa (esim. biologian, lääketieteen ja immunologian sovelluksissa) monimutkaisen systeemin globaalin käyttäytymisen kuvaamiseen, missä kokonaisuus koostuu moninaisista lokaaleista prosesseista.
Useimmiten tämä tehdään kokoamalla olemassa olevia alimalleja ja lisäämällä niihin yksityiskohtia, mikä on yleinen toimintatapa ohjelmistokehityksessä. Tästä on harvemmin hyötyä biologiassa, koska alimallit eivät ole kytkettyjä toisiinsa ominaisuuksiensa perusteella. Silloin kokonaismalli jää epäyhtenäiseksi alimoduulien kokoelmaksi ja sen vastaavuus osamallien kokeellisiin tuloksiin rajalliseksi, vaikka alimallit olisivatkin viritettyjä vastaamaan kokeellista dataa hyvin. Siksi tätä mallin sovittamista täytyy toistaa, mikä monimutkaistaa laskentaa ja vaatii onnistuakseen entistä enemmän uutta dataa.
Tässä työssä kehitimme kompleksisen mallin lisäämällä perusmalliin yksityiskohtia ja varmistamalla laskennallisia ominaisuuksia, kuten vastaavuutta kokeellisiin tuloksiin, vaiheittain. Käytimme tarkoitukseen formaalista mallinnusmenetelmää Event-B, joka tarjoaa keinon mallin asteittaiseen parantamiseen. Tämä on ensiarvoisen tärkeää laajojen mallien kehittämiselle.
Aloitamme perusmallista, jossa yksityiskohtia on rajoitetusti, ja lisäämme mallin tuottamaa informaatiota askeleittain uusilla ominaisuuksilla. Menetelmällä Event-B tuotetut osamallit ovat formaalisesti riippuvaisia toisistaan parannusvaiheiden läpi ja osamalleja voidaan myös soveltaa kaikissa näissä vaiheissa. Menetelmään Event-B kuuluu tukityökalu Rodin, jolla suoritetaan mallin formaalinen verifiointi mallintamisen joka vaiheessa. Tietääksemme tämä työ on ensimmäinen, jossa menetelmää Event-B on käytetty biologisten systeemien mallintamiseen.
Muhammad Usman Sanwal väittelee tohtoriksi perjantaina 17. huhtikuuta 2020 klo 13. Vallitsevien olosuhteiden vuoksi väitöstilaisuutta ei voi seurata paikan päällä, sen sijaan sitä on mahdollista seurata etänä seuraavan linkin kautta: https://aboakademi.zoom.us/j/616584778. (Käytännön ohjeet alla.) Vastaväittäjänä toimii Dr. David Šafránek, Masaryk University, Tšekki, ja kustoksena dosentti Luigia Petre, Åbo Akademi.
Muhammad Usman Sanwal on syntynyt 5.1.1985 Veharissa, Pakistanissa. Hän suoritti MSc-tutkinnon 2012 National University of Sciences & Technology (NUST) -yliopistossa, Islamabadissa, Pakistanissa.
Muhammad Usman Sanwal on tavoitettavissa puhelimitse numerosta 046 520 9777 ja sähköpostitse osoitteesta muhammad.sanwal@abo.fi.
Väitös on sähköisessä muodossa Doriassa: https://www.doria.fi/handle/10024/176640?locale=lfi.
Klikkaamalla kuvaa saat ladattua painokelpoisen kuvan väittelijästä.
Kuva on tiedotusvälineiden vapaasti käytettävissä.
Käytännön ohjeet tohtorinväitöstilaisuuden seuraamiseksi etänä
Jotta voisit seurata tohtorinväitöstilaisuutta etänä, tarvitset ohjelman nimeltä Zoom tai Google Chrome -selaimen. Sinun ei tarvitse luoda Zoom-tiliä tai kirjautua voidaksesi seurata väitöstilaisuutta. Jos asennat Zoom-sovelluksen tulee sinun napauttaa tapahtuman ylläolevaa linkkiä ja hyväksyä, että Zoom avaa linkin.
Väitöstilaisuuden aikana yleisön tulee varmistaa, että oman laitteen mikrofoni on mykistettynä ja että kamera ei ole päällä.
Tilaisuuden lopussa yleisö saa mahdollisuuden esittää kysymyksiä. Jos sinulla on kysymys, ilmoita siitä käyttämällä ”Raise Hand” -toimintoa. Valmistaudu etukäteen: varmista, että tietokoneessasi on mikrofoni, tai muotoile kysymys valmiiksi tekstitiedostoon, josta sitten voit kopioda sen Zoomin keskusteluosioon. Huomioi, että yleisö ei saa esittää mahdollisia teknisiä ongelmia koskevia kysymyksiä.