Andreas E. Dalsgaard

Ph.d.-studerende, cand.scient i datalogi, 28 år

Andreas Dalsgaard

Fagområde

Datalogi

Forskningsprojekt

Sammenspil mellem statisk programanalyse og model checking – målrettet udvikling af moderne sikkerhedskritiske systemer

 

Hvordan opstod din interesse for dit forskningsfelt?

Min interesse for sammenspillet mellem statisk programanalyse og model checking stammer fra mit speciale. Specialet handler om at finde tidsgrænser for indlejrede systemer. Sammen med to andre studerende viste jeg, at det var muligt at benytte en kombination af statisk programanalyse og model checking til at finde tidsgrænser og sikre, at systemerne virker korrekt. Et typisk eksempel er at sikre, at udløsningen af en airbag sker på det rigtige tidspunkt. Dette skal ske med stor nøjagtighed for at redde passagerens liv.

Hvad er de forskningsmæssige udfordringer og perspektiver ved dit projekt?

Model checking af tidsautomater og statisk programanalyse har tidligere været anvendt til udvikling af sikkerhedskritiske systemer. Ved at søge nye måder at kombinere de to teknikker på er målet at fremme teknikker til udvikling af fremtidens sikkerhedskritiske systemer, der vil være større og mere komplekse, end de er i dag. En del af dette vil være at undersøge muligheden for udviklingen af en distribueret model checker. Adskillige distribuerede model checkere er igennem tiden blevet udviklet til forskellige formalismer. Det har dog vist sig, at være svært at udvikle en skalerbar tidsautomat model checker, der kan udnytte moderne hardware.

Hvortil ønsker du at rejse med midlerne fra stipendiet?

I forbindelse med udviklingen af en distribueret tidsautomat model checker vil et længerevarende ophold ved model checking gruppen på Twente Universitet være af stor interesse. De har stor erfaring med model checking teknikker både teoretiske og praktiske perspektiver. De har tidligere udviklet en distribueret udgave af en general model checker, som de har udviklet over de sidste 10 år. Endvidere vil det muliggøre rejser til samarbejdspartnere i Tyskland.

Hvor længe skal du være væk, og hvad forventer du at få ud af opholdene?

Jeg forventer, at det sammenlagt vil dreje sig om seks til otte måneder. Forventningerne til opholdet er, at vi i samarbejde vil kunne udvikle en distribueret tidsautomat model checker, der kan udnytte moderne hardware.

Fødested, gymnasium og bopælskommune

Skelund, Aalborg tekniske Gymnasium, Aalborg

Ph.d.-projektets titel

Safety Critical Systems: Scalable Verification

Kontaktoplysninger

Telefon 99 40 98 59/60 11 08 68. E-mail: andrease@cs.aau.dk

Forskningsinstitution

Aalborg Universitet, Institut for datalogi, Selma Lagerlöfs Vej 300, 9220 Aalborg Ø

Senest opdateret 26. januar 2015