Department of Computer Science

På Aalborg Universitet har forskere og studerende på Institut for Datalogi igennem mere end et årti udviklet værktøjet TAPAAL, der netop er en modeltjekker, og de seneste år har de markeret sig blandt verdens bedste i den prestigefyldte internationale konkurrence i modeltjekning

AAU er blandt verdens bedste til at udvikle it-værktøjer, der forhindrer fatale fejl i din hverdag

De senere år har forskere fra Aalborg Universitet markeret sig som nogle af de bedste til at udvikle værktøjer, der kan forhindre, at komplekse it-systemer laver potentielt dyre eller fatale fejl. Nu har studerende videreudviklet på et eksisterende værktøj og hjemtaget guldmedaljen ved en prestigefyldt konkurrence i modeltjekning.

Det kan være dyrt at lave fejl. Spørg bare teknologigiganten Intel. I 1994 sendte de en fejlbehæftet chip på markedet, og tilbagekaldelsen af den resulterede i et milliardtab for virksomheden. I bagklogskabens lys ville de nok have ønsket sig, at de havde forudset fejlen.

De seneste 30 år er man i langt højere grad begyndt at lave computermodeller af forskellige ting eller situationer for at teste dem til bunds i en virtuel verden, inden man implementerer eller sætter det i produktion.

På Aalborg Universitet har forskere og studerende på Institut for Datalogi igennem mere end et årti udviklet værktøjet TAPAAL, der netop er en modeltjekker, og de seneste år har de markeret sig blandt verdens bedste i den prestigefyldte internationale konkurrence i modeltjekning. I år er ingen undtagelsen, og holdet bag hjemtog i begyndelsen af juni to guld-, to sølv- og en bronzemedalje:

- Det er ikke nok, at vi har en masse digitale modeller. Vi har også behov for værktøjer, der ved hjælp af komplekse beregninger kan optimere eller stressteste dem – og det er det, vi har udviklet. TAPAAL kan bruges til at tjekke, om en model virker, som den skal og opfylder de krav, der er sat.  Det er afgørende i kritiske og komplekse systemer, hvor det enten koster mange penge eller potentielt liv at lave fejl. F.eks. er det afgørende, at det system, der styrer togdriften, ikke svigter og ved en fejl får to tog til at kollidere, siger adjunkt Peter Gjøl Jensen, der er en af hovedkræfterne bag TAPAAL.

En bemærkelsesværdig indsats

Det bemærkelsesværdige ved udfaldet af årets konkurrence er, at to grupper af specialestuderende har deltaget med en videreudvikling af TAPAAL – og det har for første gang sikret Aalborg Universitet guld i kategorien LTL.

LTL eller lineær temporal logik er en særlig form for modeltjekning, hvor man tester komplekse modeller i forhold til uendelig opførsel. Tag eksempelvis et lyskryds. Her er det vigtigt, at vi i det uendelige kan være sikre på, at lyssignalet skiftet fra grøn til gul, inden det skifter til rødt, eller at krydsende trafikanter aldrig har grønt samtidig.

Ifølge Peter Gjøl Jensen, der sammen med professor Jiri Srba har vejledt de studerende, er der ingen tvivl om, at det er bemærkelsesværdigt, at de unge danskere hiver guldmedaljen hjem:

- Det er virkelig markant, at de studerende på bare et år har kunnet løfte det her værktøj til at blive det vindende i kategorien. Der er mange brikker, der skal falde på plads. For det første har de lavet et hammergodt stykke arbejde, men de bygger også videre på andre virkelig dygtige studerendes indsats.

Konkurrerer mod fagfolk med mange års erfaring

En af de studerende er Nikolaj Jensen Ulrik, der skal fortsætte som ph.d.-studerende på Institut for Datalogi. For ham har deltagelsen i konkurrencen været en stor drivkraft i specialeskrivningen:

-  Da vi snakkede om det ved første vejledermøde, virkede det som et fjernt mål at vinde konkurrencen. For vi konkurrerer mod professionelle fagfolk, der har mange års erfaring. Men det viser bare, hvor godt værktøjet har været fra begyndelsen, og det har virkelig været fedt at få mulighed for at kombinere teori og praksis.

Det anerkender Peter Gjøl Jensen. Men det siger ifølge ham også noget om de studerendes kompetencer:
 
- Det er et meget kompetitivt miljø – det er ikke nok bare at bygge software, der kan køre nogenlunde hurtigt. Man skal have øje for detaljerne. Og det har de her studerende – de ved, hvordan man bygger hurtigt og effektivt software og kan argumentere for, at det også er formelt korrekt. Det er enormt givende og afgørende i udviklingen af fremtidens software.

__________________________________________________________________________________

Vil du vide mere?

TAPAAL er et værktøj til modellering, simulering og verifikation af modeller i formatet petri-net, og over de seneste år har over 40 forskere og studerende fra Institut for Datalogi på Aalborg Universitet bidraget til udviklingen af programmet.

Model Checking Contest er en årlig konkurrence, hvor et forskerteam sammenligner værktøjer i forskellige kategorier i henhold til udvalgte benchmarks for at udpege dem, der er bedst til at håndtere givne typer problemer, f.eks. tilgængelighed. Se og læs mere her.

TAPAAL-projektet ledes af professor Jiri Srba.

De studerende bag videreudviklingen af TAPAAL er: Nikolaj Jensen Ulrik og Simon Mejlby Virenfeldt, der har arbejdet med LTL – og Peter Haahr Taankvist, Alexander Bilgram Kristensen og Thomas Pedersen, der har arbejdet med CPN (farvede petri-net)

Vejledere: Professor Jiri Srba og adjunkt Peter Gjøl Jensen.

Kontakt

Professor Jiri Srba
Institut for Datalogi, Aalborg Universitet
Telefon:2045 3514
E-mail: srba@cs.aau.dk

Adjunkt  Peter Gjøl Jensen
Institut for Datalogi, Aalborg Universitet
Telefon:6154 7278
E-mail: pgj@cs.aau.dk

Department of Computer Science, Aalborg University

Selma Lagerlöfs Vej 300  ・ 9220 Aalborg East, Denmark 
Telephone: +45 9940 9940  ・ Mail: info@cs.aau.dk

Contact department management