Populærvidenskabelig titel på dit projekt LASSO:
hvordan man tæmmer fremtidens brug af IT i alting
Hvad handler dit projekt om?
Software, hardware og kommunikationsteknologi bliver i stigende grad integreret i alverdens smarte produkter og processer med henblik på øget komfort, forbedret ydeevne, funktionalitet og brugbarhed samt reduceret ressourceforbrug.
Den hastige vækst i kompleksitet af disse systemer vanskeliggør imidlertid dette. LASSO har som målsætning at frembringe en ny generation af skalerbare værktøjer til model-baseret læring, analyse, syntese og optimering af cyber-fysiske systemer baseret på et matematisk sundt grundlag, der vil gøre det muligt at foretage afvejninger mellem korrekt funktionalitet og optimeringsønsker. LASSO har som hypotese, at en fuld integration af ”model checking” og ”machine learning” vil være nøglen til nye innovative, skalerbare metoder og værktøjer til læring, analyse, syntese og optimering af cyber-fysiske systemer.
Hvordan opstod din interesse for dit forskningsfelt?
Jeg var ph.d.-studerende i 1983-85 ved Edinburgh Universitet, hvor jeg under vejledning af professor Robin Milner arbejdede på det matematiske grundlag for semantik af parallelle systemer. Her var fokus på forskellige begreber af korrekthed. Ved slutningen af ph.d.-studiet fik jeg den ide, at man kunne lave et værktøj, dvs. en algoritme, der givet beskrivelser af det parellelle system og dets specifikation automatisk ville afgøre korrektheden. Hjulpet af min første bevilling i 1987 fra daværende Statens Naturvidenskabelige Forskningsråd blev det til mit første verifikationsværktøj, der siden er blevet efterfulgt af flere effektive værktøjer, heriblandt UPPAAL, der muliggør automatisk verifikation af tidsmæssige krav, f.x. af det software, der anvendes i biler.
Hvad er de forskningsmæssige udfordringer og perspektiver ved dit projekt?
For at LASSO kan nå sit mål, vil det være afgørende, at effektiviteten og anvendeligheden af eksisterende automatiske verifikations- og synteseteknikker forbedres radikalt, blandt andet gennem vidtrækkende og ambitiøse kombinationer med ”machine learning”-teknikker. Dette afføder en række forskningsmæssige udfordringer. Modellering af cyber-fysiske systemer kræver, at klassiske, diskrete datalogiske modeller udvides med en række kvantiteter, såsom tid, energi og stokastik. Desværre er automatisk verifikation af korrekthed for denne type modeller uafgørbar, hvorfor der er behov for udvikling af en lang række nye approximative og statistisk baserede verifikationsmetoder. Statistisk verifikation i sig selv, om end yderst lovende, har sine egne udfordringer, blandt andet i effektiv og præcis estimering af såkaldte ”rare events”. Det er blandt andet her, at inddragelsen af ”machine learning” forhåbentligt vil kunne bidrage med løsninger.
Hvad betyder en Advanced Grant for din fremtidige karriere?
I forhold til de mine mange øvrige projekter, betyder en Advanced Grant, at der bliver mere tid og plads til reel grundforskning. De verifikationsværktøjer, jeg har udarbejdet gennem de sidste 20 år, har nået en stor modenhed, hvor de i stigende grad anvendes af virksomheder, der beskæftiger sig med indlejret software. For at kunne skalere til fremtidens IoT-baserede og cyber-fysiske systemer er der imidlertid brug for nye grundforskningsmæssige landvindinger, hvilket LASSO præcist giver mig mulighed for. Samtidigt føler jeg det som en stor anerkendelse at få en Advanced Grant, hvilket omvendt også giver store (egne) forventninger til min fremtidige forskning.
Lidt om mennesket bag forskeren
Jeg er født og opvokset i Aalborgs vestby, hvor jeg hurtigt blev hooked på fodbold i den lokale klub Aalborg Freja, parallelt med en lige så stor passion for sportsdans. Efter min ph.d.-uddannelse ved CMU og Edinburgh Universitet kom jeg ”hjem” til Danmark, hvor jeg indtil for fire år siden boede i den lille stationsby Arden med min kone Merete og vore to døtre, Mia og Trine. Her blev oldboys fodbold suppleret med tennis, volleyball og ikke mindst badminton i den lokale klub Jarl Arden, der blev et andet hjem for hele familien. Jeg er i de sidste tre år blevet morfar til Sif, Sofia og Vilja og begyndt på vinterbadning.
Fagområde
Datalogi
Gymnasium og bopælskommune
Hasseris Gymnasium, bopæl i Aalborg
Kontaktoplysninger
Telefon: 9940 8893, e-mail: kgl@cs.aau.dk
Forskningsinstitution
Aalborg Universitet, Institut for Datalogi