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 environment before implementing them in real-life production. At the Department of Computer Science, Aalborg University, researchers and students have been developing such a model checking tool, named TAPAAL, for more than a decade.
Being able to test critical and complex systems in a virtual setting is crucial in order to avoid potentially life-threatening errors.
- 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, says Assistant Professor Peter Gjøl Jensen.
Theory and practice
In recent years, TAPAAL has gained a strong position among the world’s model checking tools and has now added to an already impressive track record in the prestigious international Model Checking Contest: On June 21, the team behind TAPAAL brought home three gold medals and two silver medals.
The three gold medals are very much a result of the work of three students graduating in June 2022 from the Computer Science education: Jesper A. van Diepen, Nicolaj Ø. Jensen and Mathias M. Sørensen. Working on TAPAAL was part of their master’s thesis.
- One of the projects that we could select dealt with Petri Nets, which is a mathematical modelling language for the description of distributed systems. I think it is an interesting topic, and it also appealed to me that it would be possible to combine theory and hands-on work on TAPAAL, says Jesper A. van Diepen.
To Mathias M. Sørensen, the combination of theory and practice was also appealing:
- There is obviously a large part of our master’s thesis that explores the theory behind Petri Nets, but it has been really great to be able to apply the theory to a concrete tool and see that it actually works.
The work of the three students has resulted in a new initial phase in the tool where the given Petri Net model is simplified, which enhances the performance of the following phases while very importantly, preserving the quality of the model check. The enhanced performance meant that TAPAAL grabbed the gold medal in the category Reachability, which is the most competitive category at the Model Checking Contest.
- The Reachability category represents the most fundamental problem to be solved: How fast can your tool detect an error state in a given model? With this enhancement of the performance, TAPAAL is able to test larger and more complex systems, Nicolaj Ø. Jensen explains.
According to Peter Gjøl Jensen, the enhancement has taken TAPAAL to a level that opens up for new and very interesting perspectives:
- Previously, our tool struggled with big distributed systems like that of a larger train station. With this enhancement, we are able to verify larger and even more complex systems. It could be the interaction between medical devices like pacemakers and smart insulin pumps or the multiple components in an aircraft that need to coordinate properly in order to ensure that the landing gear is lowered.
To Peter Gjøl Jensen, who – together with Professor Jiri Srba – supervised their work on TAPAAL, the enhancement to TAPAAL was an impressive feat on the part of the three students:
- It is striking how these three students in just one year have been able to further develop this tool to be the winner of three categories in such a tough competition. They really did a terrific job, but it is also important to say that their work builds upon the work of other excellent students at our department.
In addition to the gold medal in the Reachability category, TAPAAL won the CTL Examinations and LTL Examinations categories. The two silver medals were won in the categories Upper-bounds and Global properties.
- 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 reachability.
- 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.
- The TAPAAL project is headed by Professor Jiri Srba.
- The students who worked on the further development of TAPAAL are Jesper A. van Diepen, Nicolaj Ø. Jensen and Mathias M. Sørensen. Supervisors: Professor Jiri Srba and Assistant Professor Peter Gjøl Jensen.
- For more info on TAPAAL, check tapaal.net