Department of Computer Science

In recent years, researchers from Aalborg University have gained a strong position among the world’s leading developers in the prestigious international Model Checking Contest.

AAU among the world’s best developers of verification tools that prevent everyday systems from making fatal mistakes

In recent years, researchers from Aalborg University have built an impressive track record as leaders within the development of tools that prevent complex IT systems from making potentially expensive or fatal mistakes. Now, students have made further developments on an existing tool and taken home the gold medal at a prestigious model checking contest.

Making mistakes can be expensive. Just ask tech giant Intel. In 1994, they put a defective chip on the market, and the subsequent recall resulted in a billion-dollar loss for the company. In hindsight, they probably wished they could have predicted the defect.

Over the last 30 years, computer models have been increasingly used for modelling devices or situations in order to test them thoroughly in a virtual world before implementing them or putting them into production.

At Aalborg University, researchers and students at the Department of Computer Science have been working on just such a tool, named TAPAAL, for more than a decade. In recent years, they have gained a strong position among the world’s leading developers in the prestigious international Model Checking Contest. This year is no exception: In early June, the team behind TAPAAL brought home two gold, two silver and one bronze medal:

- Having a lot of digital models is not enough. We also need tools that use complex calculations to optimise or stress test the models – and that is exactly what we have developed. TAPAAL can be used for checking whether a model works the way it is supposed to, and whether it fulfils the necessary requirements. This is crucial in terms of critical and complex systems where mistakes may either cost a lot of money or potentially even human lives. For instance, it is crucial that the system controlling train operations does not malfunction and make two trains collide because of a system error, Assistant Professor Peter Gjøl Jensen, one of the leading researchers behind TAPAAL, says.

A remarkable effort

The remarkable thing about the result of this year’s competition is that two groups of master’s students participated with an extension of TAPAAL – and this led to Aalborg University winning the gold medal in the category LTL for the first time.

LTL, or linear temporal logic, is a particular type of model checking in which complex models are tested with regards to infinite behaviour. Picture a set of traffic lights. In this system, it is important that we can be certain to an infinite degree that the lights will change from green to yellow before they change to red, or that the lights at crossing roads are never green simultaneously.

According to Peter Gjøl Jensen, who supervised the students with Professor Jiri Srba, there is no doubt that the young Danes taking home the gold is a remarkable feat:

- It is striking how the students in just one year have been able to elevate this tool to be the winner of the category. A lot of pieces have had to fall into place. First of all, they themselves did a terrific job, but their work is also built upon the work of other excellent students.

Competing against experts with years of experience

One of the students is Nikolaj Jensen Ulrik, who will now continue his work as a PhD student at the Department of Computer Science. To him, participating in the contest was a major driving force in completing his master’s thesis:

- When we talked about it at our very first supervisory meeting, winning a contest seemed a distant goal, because we are competing against professional experts with several years’ experience. But this just goes to show how good this tool has been from the very start, and it has been amazing to get this opportunity to combine theory and practice.<<

Peter Gjøl Jensen acknowledges this point. But he also underlines how the result reflects the students’ own competences:
 
- It is a highly competitive environment – You do not get far just by building software that runs at a fairly high speed. You need to have an eye for details. And that is what these students have – They know how to build fast and efficient software, and they can carry an argument on how it is formally correct as well. This is enormously rewarding and a crucial ability when developing the software systems of the future.

__________________________________________________________________________

Want to know more?

TAPAAL is a tool for modelling, simulation and verification of models in the format Petri Nets, and over the last years, more than 40 researchers and students from the Department of Computer Science have contributed to the development of the programme.

Model Checking Contest is an annual contest in which a research team compare tools within different categories on the basis of a range of benchmarks, in order to select those best suited for handling specific kinds of problems, such as accessibility. For more information, visit this website.

The TAPAAL project is headed by Professor Jiri Srba.

The students who worked on the further development of TAPAAL are: Nikolaj Jensen Ulrik and Simon Mejlby Virenfeldt, who worked with LTL – and Peter Haahr Taankvist, Alexander Bilgram Kristensen and Thomas Pedersen, who worked with CPN (Coloured Petri Nets)

Supervisors: Professor Jiri Srba and Assistant Professor Peter Gjøl Jensen.

FOR MORE INFORMATION, CONTACT:

Professor Jiri Srba
Department of Computer Science
Aalborg University
Phone:  2045 3514
E-mail: srba@cs.aau.dk

Assistant Professor Peter Gjøl Jensen
Department of Computer Science
Aalborg University
Phone: 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