De fleste af os er ikke bevidste om det i vores daglige liv, men vi er omgivet af det, der kaldes cyber-fysiske systemer. Kort forklaret er det systemer, hvor software- og hardwarekomponenter kommunikerer med og styrer en fysisk virkelighed. Det kan være vindmøller, biler eller noget så livsvigtigt som en pacemaker. 

Men når vi anvender komplekse indlejrede it-systemer, er det afgørende, at de er pålidelige og robuste. Vi må kunne stole på, at de fungerer fejlfrit. For eksempel skal en airbag udløses inden for få mikrosekunder, uanset hvornår en potentielt farlig kollision måtte ske, og uafhængigt af hvilke andre processer der måtte være i gang.

I mere end 25 år har UPPAAL, et værktøj til analyse og model checking, været et af de mest anvendte værktøjer til verifikation af realtidsmodeller både i akademiske kredse og i industrien. Nu er en ny og forbedret version, UPPAAL 5.0, tilgængelig. Det blev markeret ved en reception på Aalborg Universitet fredag 23. juni.

FRA TRAFIKLYS TIL STYRING AF CORONA-INITIATIVER

En af hovedarkitekterne bag systemet er Kim Guldstrand Larsen, professor ved Institut for Datalogi på Aalborg Universitet. Han var en af grundlæggerne af værktøjet i 1995 i et samarbejde mellem Aalborg Universitet og Uppsala Universitet.

- Jeg er meget stolt af, at vi i dag kan lancere en ny version, hvor vi samler de fleste af værktøjerne, der er udviklet under UPPAAL-paraplyen, i ét. Vi har gentagne gange demonstreret, hvor effektivt UPPAAL er som værktøj, og det er blevet brugt i utallige sammenhænge, lige fra trafikstyring til fjernvarmeregulering, håndtering af regnvand og corona-initiativer. Det er et fremragende eksempel på, hvordan noget, der er teoretisk forankret, samtidig har høj anvendelsesværdi for både virksomheder og samfund, forklarede Kim Guldstrand Larsen ved arrangementet.

Som led i receptionen blev der også vist videohilsner fra kolleger fra Tyskland, Østrig, Island, Kina, Sverige og USA. Alle sammen folk, der enten anvender UPPAAL eller har været involveret i udviklingen af det.

Og netop den kontinuerlige udvikling af værktøjet blev fremhævet flere gange. I sin tale understregede Kim Guldstrand Larsen, hvordan det nuværende system er resultatet af mange menneskers hårde arbejde:

- Det er også takket være disse kolleger, at vi i dag har en værktøjskasse fyldt med virkelig gode redskaber til at simulere, teste og verificere modeller og systemer.

VEKSELVIRKNING MELLEM FORSKNING OG ANVENDELSE

En anden taler ved arrangementet, Peter Axel Nielsen, institutleder ved Institut for Datalogi på Aalborg Universitet, påpegede, at den langvarige holdindsats er noget helt særligt:

- På den måde er det et ret unikt stykke software, men det er også en unik tilgang til forskning. Derudover har det været afgørende for succesen, at udviklingen har bevæget sig mellem forskning og teori på den ene side og anvendelse i konkrete tilfælde på den anden side. Den vekselvirkning er enormt vigtig.

Det nuværende hold af forskere, der arbejder med udviklingen af UPPAAL, tæller foruden Kim Guldstrand Larsen også Marius Mikučionis, Falke Carlsen, Thorulf Neustrup, Sean Kristian Remond Harbo og Kenneth Yrke.