Model Based System Development/Research Themes/Computer-Aided Verification and Analysis

Timed Automata Model Checking

Model checking is emerging as a practical tool for automated debugging of complex reactive systems such as embedded controllers and network protocols. In model checking, specifications about the system are expressed as (temporal) logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. Extremely large state-spaces can often be traversed in minutes. In 2007, Edmund M. Clarke, E. Allen Emerson and Joseph Sifakis were awarded the ACM Turing Award for their roles in developing model checking into a highly effective verification technology, widely adopted in the hardware and software industries. In our research, we concentrate on the case where systems are described as networks of timed automata in the sense of Alur and Dill. During the last decade, there has been an immense progress in the area of timed model checking. Our group is one of the two or three leading groups worldwide in the area of applying timed automata model checking to industrial sized problems in the area of embedded and distributed systems. In part due to our work, tools such as Uppaal are now routinely used for industrial case studies.

In our research, we follow an iterative approach where fundamental research on theory and algorithms - challenged by real-life case-studies - is developed and implemented in methods and tools, which are evaluated again through case studies. This research cycle is very labor intensive and for that reason we have decided not to develop our own model checking tool. Instead, we closely collaborate with the team of prof. Kim Larsen of Aalborg University on adding new functionality to the Uppaal model checker. This collaboration is supported by the European projects projects AMETIST (that we coordinated) and Quasimodo. At the national level our research is supported by the PROGRESS project HaaST, NWO projects FRAAI and ARTS, and by the ESI project OCTOPUS.

We have proposed and implemented (together with the team of prof. Larsen) several extensions of Uppaal, such as distributed model checking (2000), guided model checking (2001). and parametric model checking (2002). More recently, we enhancement Uppaal with symmetry reduction (2004) using the scalarset datatype known from Murphi. For all examples that we experimented with (both academic toy examples and industrial cases), we obtained a drastic reduction of both computation time and memory usage, exponential in the size of the scalar sets used. Thus, for instance, we discovered that the Bang & Olufsen audio/video protocol that was previously proven to be correct for two processes in [HSLL97] actually exhibits faulty behavior for three processes. Our team coauthors the latest Uppaal 4.0 release in which this extension has been implemented [QEST06]. We have also developed a formalism that enables compositional abstraction on networks of timed automata, and proved it to be a very effective method to combat the state space explosion problem in real-time model checking. This technique, for instance, made it possible to verify the Zeroconf protocol for an arbitrary number of hosts [BGV07].

We also pioneered the use of model checking in a freshman's course on operating systems and in a course for high school students.

Timed and Hybrid I/O Automata

Hybrid systems are systems that exhibit a combination of discrete and continuous behavior. Typical hybrid systems include computer components, which operate in discrete program steps, and real-world components, whose behavior over time intervals evolves according to physical constraints. Important examples of hybrid systems include automated transportation systems, robotics systems, process control systems, systems of embedded devices, and mobile computing systems. Such systems can be very complex, and very difficult to describe and analyze. In close collaboration with the group of Prof. Nancy Lynch at the Massachusetts Institute of Technology and prof. Roberto Segala from the University of Verona, we developed the timed and hybrid I/O automata frameworks. These basic mathematical frameworks support description and analysis of timed and hybrid computer based systems. The TIOA and HIOA frameworks have been widely used, amongst others, to analyze automated transportation systems, intelligent vehicle highway systems, air traffic control systems, automotive control systems, consumer electronics applications, and wireless ad hoc networks. Our paper [LSV03] on the HIOA framework has 313 cites in Google Scholar (March 2009). Together with Dilsun Kaynar, Nancy Lynch and Roberto Segala, we also wrote a monograph on the TIOA framework [KLSV06]. A toolset supporting our TIOA framework, which includes embeddings of TIOA into PVS and Uppaal, has been developed by VeroModo Inc.

A different line of research was followed by our PhD student Goran Frehse in his thesis on the hybrid automata model checker PHAVer [Fre05]. Experiments show that PHAVer computes faster and more accurately than other, comparable programs, such as the widely used HyTech tool from the University of Berkeley.

Probabilistic Automata

Nondeterminism is a key feature in models for concurrent and reactive systems. It allows us to express that often we do not know (or do not care) which events will occur or in which order certain events will occur. Randomization is similar but nevertheless distinctly different from nondeterminism, and plays an essential role in many distributed algorithms. Probabilistic automata (PAs), proposed by Segala in his PhD thesis from '95, constitute a general framework for modeling and analyzing discrete event systems that exhibit both nondeterministic and probabilistic behavior, such as distributed algorithms and network protocols. The behavior of PAs is commonly defined using schedulers (also called adversaries or strategies), which resolve all nondeterministic choices based on past history. From the resulting purely probabilistic structures, trace distributions can be extracted, whose intent is to capture the observable behavior of a PA. Technically, the combination of nondeterministic and probabilistic turns out to be involved. We established a number of fundamental results about probabilistic automata.

In a paper presented at ICALP'03 [SV03], we presented a simple and intuitive testing scenario for image finite probabilistic automata. This work received the EATCS Best Paper Award. A journal version of this paper was published in JACM [CSV07]. For her contribution to this paper, Mariëlle Stoelinga received the 2008 Professor De Winter prize. Together with Nancy Lynch and Roberto Segala, we established that the simulation preorder is in fact the coarsest refinement of the trace distribution preorder that is compositional for probabilistic automata [SIAM07]. This result was the starting point for the PhD research of Ling Cheung, who proposed various restricted notions of schedulers for which trace inclusion is compositional. In 2006, Ling Cheung was awarded a PhD degree cum laude for her thesis "Reconciling Nondeterministic and Probabilistic Choices".

In 2007 David Jansen joined our group as assistent professor, bringing in considerable expertise on probabilistic model checking, an area where we see many important challenges.

Our work on probabilistic systems took place in the context of the NWO-DFG bilateral cooperation projects VOSS1 and VOSS2, and is currently supported by the EU FP7 project Quasimodo.

Model Based Testing

Quality of software is an issue of increasing importance and growing concern. Systematic testing of software plays an important role in the quest for improved quality. Testing, however, turns out to be expensive and time consuming. One source of problems is the often imprecise and ambiguous nature of specifications, so that a good basis for testing is missing. Another reason is the usually manual and laborious testing process without effective automation, so that testing is error-prone and consumes many resources.

Current research efforts in model based testing aim at contributing to solutions for these testing problems. The starting point for model based testing is a formal description, or model, of the system under test. On the one hand, such a model serves as a precise and complete specification, and, consequently, is a good basis for testing. On the other hand, such models can be automatically processed by tools, which allows to effectively automate the testing process. In particular, algorithms have been developed to generate tests from such formal models. Tools, implementing these algorithms, lead to automatic, faster and less error-prone test generation: millions of test events can be automatically generated, and `on-the-fly' executed, and analysed.

Model based testing is an important aspect of the project TANGRAM, which is a joint research and development effort of a couple of universities and companies, coordinated by the Embedded Systems Institute, in which ASML is the core industrial partner.