In embedded concurrent systems, you may have thousands of tasks running in parallel all drawing on the same limited resources. Just take the very concrete example of a modern car: The number of tasks controlling everything from fuel consumption to engine emissions, tyre pressure and assisted braking is way higher than the number of computers installed in the car. This means that tasks need to be stopped and restarted constantly to make use of the available shared resources according to the deadlines set for each task.
- It may sound odd that you wish to stop time. But let us say that the task of checking and adjusting engine emissions takes approximatively 10 milliseconds, and it was interrupted after 3 milliseconds, because a task with a much tighter deadline, for example activating the brakes to avoid a collision, needed the resources to execute the task. When resources are available again to check and adjust engine emissions, you need to know that only approximately 7 milliseconds remain before the task is fully executed - in order words, you need a stop watch function, Kim Guldstrand Larsen, Professor at the Department of Computer Science, Aalborg University, explains and he continues:
- What we are basically dealing with here is a real-time operating system where missing a deadline is simply not an option. Our paper demonstrates how you can avoid missing task deadlines in practice, which is absolutely crucial in order to ensure the correct and safe functioning of the many embedded concurrent systems that we use in our everyday lives.
Uppaal, a world-renowned integrated tool environment for modelling, validation and verification of real-time systems, offers efficient support for automated verification of models using the stop watch mechanism described in the paper.
The CONCUR conference is the flagship conference within the field of embedded concurrent systems. The Test-of-Time Award was initiated in 2020 by the Steering Committee of CONCUR and the IFIP (International Federation for Information Processing) Working Group 1.8 on Concurrency Theory to recognize important achievements in Concurrency Theory published at CONCUR. All papers of the period 1998-2003 were eligible for this year's awards. In an extract from the jury´s laudation of the paper, it says:
“The paper "The Impressive Power of Stopwatches" studies the expressive power of timed automata enriched with stopwatches and unobservable behaviours. Surprisingly, it is proved with smart constructions that this seemingly mild extension already reaches the full expressive power of linear hybrid automata, a very powerful model using a finite discrete control together with continuous variables, linear guards and linear updates.”
Years of collaboration
Kim Guldstrand Larsen and Franck Cassez, who is currently a Lead Researcher at ConsenSys Quorum Protocol Engineering, have collaborated on a number of European projects and research papers over the years, their latest paper being “Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction” co-written with Peter Gjøl Jensen, Assistant Professor, Department of Computer Science, Aalborg University, published in 2021.
Both Kim Guldstrand Larsen and Franck Cassez plan to attend the conference to receive the award and deliver a talk.
- I am extremely happy and honoured to receive such a prestigious award acknowledging that this early research by Franck and me has made a significant impact on the theory and practice of concurrent systems, says Kim Guldstrand Larsen.
- The Impressive Power of Stop Watches
- CONCUR 2022 Conference
- Laudations – Test-of-Time Awards
- Personal website, Kim Guldstrand Larsen
- Personal website, Franck Cassez
Kim Guldstrand Larsen
Department of Computer Science,
Department of Computer Science,
Phone: +45 4019 7682