{"id":32717,"date":"2022-03-31T12:13:24","date_gmt":"2022-03-31T12:13:24","guid":{"rendered":"https:\/\/direc.dk\/moed-martin-zimmermann-hvis-forskning-fokuserer-paa-verifikationsvaerktoejer\/"},"modified":"2024-12-16T11:08:44","modified_gmt":"2024-12-16T11:08:44","slug":"moed-martin-zimmermann-hvis-forskning-fokuserer-paa-verifikationsvaerktoejer","status":"publish","type":"post","link":"https:\/\/direc.dk\/da\/moed-martin-zimmermann-hvis-forskning-fokuserer-paa-verifikationsvaerktoejer\/","title":{"rendered":"M\u00f8d Martin Zimmermann, hvis forskning fokuserer p\u00e5 verifikationsv\u00e6rkt\u00f8jer"},"content":{"rendered":"\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t
\n\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t\t\t
\n\t\t\t\t\t\n\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\tTil nyheder<\/span>\n\t\t\t\t\t<\/span>\n\t\t\t\t\t<\/a>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t\t\t

31. marts 2022<\/p>\n\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t

\n\t\t\t\t
\n\t\t\t\t\t

M\u00f8d Martin Zimmermann, hvis forskning fokuserer p\u00e5 verifikationsv\u00e6rkt\u00f8jer<\/h1>\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t\t\t

Den 39-\u00e5rige Martin Zimmermann fra Tyskland arbejder med korrekte og sikre systemer. Siden sommeren 2021 har han arbejdet som lektor i forskningsgruppen for Distribuerede, Embedded og Intelligente Systemer (DEIS) ved Institut for Datalogi, Aalborg Universitet.<\/p>\n\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t

\n\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t
\n\t\t\t
<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t
\n\t\t\t\t\t\t\t
<\/div>\n\t\t\t\t\t\t\t
\n\t\t\t\t\t
\n\t\t\t
\n\t\t\t\t\t
<\/div>\n\t\t\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t
\n\t\t\t
<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t
\n\t\t\t
\n\t\t\t\t\t
<\/div>\n\t\t\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t\t\tZimmermann er en del af DIREC-projektet Verifiable and Safe AI for Autonomous Systems<\/a>. Projektets m\u00e5l er at udvikle metoder og v\u00e6rkt\u00f8jer til sikkerhedskritiske systemer inden for forskellige dom\u00e6ner. Her arbejder han p\u00e5 at forst\u00e5 fundamentet for korrekte og sikre systemer.\r\n\r\nKan du fort\u00e6lle om dit forskningsomr\u00e5de?<\/b>\r\nSoftware og embedded systemer findes overalt i vores hverdag, fra medicinske enheder til fly og airbags i vores biler. Disse softwaresystemer er ofte meget komplekse, og det er udfordrende at udvikle korrekte systemer. Derfor har vi brug for verifikationssoftware, der kan tjekke s\u00e5danne systemer for fejl.\r\n\r\nNyhederne er fulde af historier om potentielle s\u00e5rbarheder i software og embedded systemer. Nogle af disse s\u00e5rbarheder har eksisteret i flere \u00e5r og er meget sv\u00e6re at finde. De er m\u00e5ske ikke synlige i daglig brug \u2013 kun n\u00e5r man fors\u00f8ger at udnytte et system.\r\n\r\nDet bliver endnu mere udtalt, n\u00e5r man ser p\u00e5 distribuerede systemer, der best\u00e5r af flere komponenter, som interagerer med hinanden. Som for eksempel et website til billetsystemet i en biograf, hvor man klikker p\u00e5 den s\u00e6de, man \u00f8nsker at reservere, mens andre g\u00f8r det samtidig. Systemet skal kunne h\u00e5ndtere mange samtidige anmodninger. Verifikation fors\u00f8ger at automatisere r\u00e6sonneringen og automatisk bevise, at systemet er korrekt og sikkert.\r\n\r\nHvordan kan vi g\u00f8re disse systemer mere sikre?<\/b>\r\nPersonligt ser jeg dette som en form for spil. Jeg vil designe et system, der lever i et milj\u00f8, s\u00e5 jeg ser det som et spil mellem systemet og milj\u00f8et. Systemet vil opfylde en bestemt egenskab, og milj\u00f8et vil fors\u00f8ge at bryde systemet. Og ved at anskue det som et spil kan man opn\u00e5 meget st\u00e6rke garantier.\r\n\r\nDet er meget sv\u00e6rt at f\u00e5 komplekse systemer til at v\u00e6re korrekte. Og hvis du har et sikkerhedskritisk system, skal du have disse garantier opn\u00e5et via verifikationssoftware. Hvis du bruger software, der styrer en airbag, vil du gerne v\u00e6re sikker p\u00e5, at det fungerer korrekt. Det er nemt at overse fejl \u2013 s\u00e5 man kan ikke stole p\u00e5, at mennesker tjekker koden.\r\n\r\nHvad er potentialet ved verifikation?<\/b>\r\nVerifikation er en meget udfordrende opgave. Det er sv\u00e6rt for et menneske at argumentere for, at et system er korrekt, og det er ogs\u00e5 sv\u00e6rt for en computer, s\u00e5 desv\u00e6rre er det ikke universelt anvendeligt. Verifikation bruges til systemer, der er sikkerhedskritiske, men selv her er der en afvejning mellem verifikationsomkostninger og udviklingsomkostninger.\r\n\r\nEt af vores m\u00e5l er at udvikle teknikker, der er nemme at bruge i praksis. Vi arbejder p\u00e5 fundamentet for verifikationssprog og fors\u00f8ger at forst\u00e5, hvor langt vi kan presse deres udtrykskraft, f\u00f8r det bliver urealistisk at verificere noget. Det kan tage timer eller dage at verificere noget, s\u00e5 det er en beregningsm\u00e6ssigt dyr opgave. Vi fors\u00f8ger at forst\u00e5, hvad der er muligt og at finde problemer og anvendelsesomr\u00e5der, hvor vi kan l\u00f8se opgaven hurtigere.\r\n\r\nEn anden vigtig ting er, at vi har brug for pr\u00e6cise specifikationssprog til verifikation. Du kan ikke bruge naturligt sprog. Verifikationsalgoritmen kr\u00e6ver en pr\u00e6cis specifikation med pr\u00e6cise semantikker, s\u00e5 vi udvikler forskellige logikker for at se, om de kan bruges af ingeni\u00f8rer til faktisk at skrive specifikationer. Hvis det er for kompliceret for praktikeren, f.eks. ingeni\u00f8ren, vil det ikke blive brugt. Man skal finde den gyldne mellemvej mellem udtrykskraft og brugervenlighed.\r\n\r\nKendte du Aalborg Universitet, f\u00f8r du blev ansat?<\/b>\r\nJeg har haft forbindelse til Aalborg siden min ph.d., hvor jeg arbejdede p\u00e5 et europ\u00e6isk projekt med partnere fra hele Europa, herunder DEIS-gruppen i Aalborg. Jeg har v\u00e6ret i Aalborg et par gange under min ph.d. og kendte folk her. Aalborg er centralt i Europa, n\u00e5r det kommer til verifikation og design af systemer. Der er mange samarbejdspartnere, og der er et godt forhold til industrien sammenlignet med andre steder. Det er et rigtig godt sted.\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t
\n\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t
\n\t\t\t\t\t\t\t\t\t

Om Martin Zimmermann<\/strong><\/p>\n