Abstract
Kim Larsen is one of the leading figures in formal verification of real-time systems, through the CISS () center he co-founded in Aalborg (Denmark). He is the architect of the UPPAAL (for Uppsala/Aalborg) verification system, which is the most powerful and widely used verification system for timed automata today. After an overview of embedded systems and formal qualitative and quantitative verification of their logical and temporal properties, he presents UPPAAL's design and main functionalities, using the example of a railway signalling system, followed by the main algorithms at work. He then illustrates the power of timed verification with a number of industrial examples: detection and correction of a very old bug that had never before been characterized in Bang & Olufsen audio/video systems, protocol verification at Philips, various automotive applications, timed task scheduling, and more.
