Zimmermann er en del af DIREC-projektet Verifiable and Safe AI for Autonomous Systems. Projektets mål er at udvikle metoder og værktøjer til sikkerhedskritiske systemer inden for forskellige domæner. Her arbejder han på at forstå fundamentet for korrekte og sikre systemer. Kan du fortælle om dit forskningsområde? Software 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ådanne systemer for fejl. Nyhederne er fulde af historier om potentielle sårbarheder i software og embedded systemer. Nogle af disse sårbarheder har eksisteret i flere år og er meget svære at finde. De er måske ikke synlige i daglig brug – kun når man forsøger at udnytte et system. Det bliver endnu mere udtalt, når man ser på distribuerede systemer, der består af flere komponenter, som interagerer med hinanden. Som for eksempel et website til billetsystemet i en biograf, hvor man klikker på den sæde, man ønsker at reservere, mens andre gør det samtidig. Systemet skal kunne håndtere mange samtidige anmodninger. Verifikation forsøger at automatisere ræsonneringen og automatisk bevise, at systemet er korrekt og sikkert. Hvordan kan vi gøre disse systemer mere sikre? Personligt ser jeg dette som en form for spil. Jeg vil designe et system, der lever i et miljø, så jeg ser det som et spil mellem systemet og miljøet. Systemet vil opfylde en bestemt egenskab, og miljøet vil forsøge at bryde systemet. Og ved at anskue det som et spil kan man opnå meget stærke garantier. Det er meget svært at få komplekse systemer til at være korrekte. Og hvis du har et sikkerhedskritisk system, skal du have disse garantier opnået via verifikationssoftware. Hvis du bruger software, der styrer en airbag, vil du gerne være sikker på, at det fungerer korrekt. Det er nemt at overse fejl – så man kan ikke stole på, at mennesker tjekker koden. Hvad er potentialet ved verifikation? Verifikation er en meget udfordrende opgave. Det er svært for et menneske at argumentere for, at et system er korrekt, og det er også svært for en computer, så desværre er det ikke universelt anvendeligt. Verifikation bruges til systemer, der er sikkerhedskritiske, men selv her er der en afvejning mellem verifikationsomkostninger og udviklingsomkostninger. Et af vores mål er at udvikle teknikker, der er nemme at bruge i praksis. Vi arbejder på fundamentet for verifikationssprog og forsøger at forstå, hvor langt vi kan presse deres udtrykskraft, før det bliver urealistisk at verificere noget. Det kan tage timer eller dage at verificere noget, så det er en beregningsmæssigt dyr opgave. Vi forsøger at forstå, hvad der er muligt og at finde problemer og anvendelsesområder, hvor vi kan løse opgaven hurtigere. En anden vigtig ting er, at vi har brug for præcise specifikationssprog til verifikation. Du kan ikke bruge naturligt sprog. Verifikationsalgoritmen kræver en præcis specifikation med præcise semantikker, så vi udvikler forskellige logikker for at se, om de kan bruges af ingeniører til faktisk at skrive specifikationer. Hvis det er for kompliceret for praktikeren, f.eks. ingeniøren, vil det ikke blive brugt. Man skal finde den gyldne mellemvej mellem udtrykskraft og brugervenlighed. Kendte du Aalborg Universitet, før du blev ansat? Jeg har haft forbindelse til Aalborg siden min ph.d., hvor jeg arbejdede på et europæisk projekt med partnere fra hele Europa, herunder DEIS-gruppen i Aalborg. Jeg har været i Aalborg et par gange under min ph.d. og kendte folk her. Aalborg er centralt i Europa, når 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.