Where: Radboud University Nijmegen
The research mission of the Informatics for Technical Applications (ITA) group is
- to carry out fundamental research on formal methods and tools for the specification, design, analysis and testing of computer systems, with focus on embedded systems, distributed algorithms and protocols;
- to demonstrate and assess the effectiveness of using these methods and tools in the industrial development process.
Characteristic of these systems are the high dependability requirements. Besides functional constraints many other aspects play a role in the design such as timeliness, fault tolerance, availability, security, and safety. An additional characteristic of embedded systems is the complex interaction with environment. One can only design and reason about embedded systems if one takes the behavior of their environment into account. Frequently this environment is highly nondeterministic and intrinsically continuous.
For more information about our research we refer to our website. Below we describe a couple of research projects that may be carried out within our group.
Project 1: Distance Detection in Video Surveillance
Automatic detection of distances between (moving) people and objects is an important topic in the use of video cameras for surveillance purposes. There are many possible application area’s, like crime detection and preventions, collision prevention in many situations, security systems for elderly people.
Research can be aimed at fundamental computer vision methods and algorithms, like distance maps, movement tracking or extracting 3D information from 1or 2 video streams. Research can also be aimed at certain application areas in order to have relevant descriptions of objects, people and situations which need to be detected with a certain performance.
Project 2: Detection of Publicity in Video Streams
A large amount of money is spent by companies on advertisements around sport events. More and more it is important for them to measure the time their boards and logos are visible on TV broadcast. Research will aim at fast and reliable detection of advertisements in video streams, going from relatively simple cases, e.g. a fixed board along the playing field, to more difficult cases, e.g. a logo on a player’s shirt.
Project 3: Advancing the use of Model Checkers in Education
Each year, thousands of Computer Science students are exposed to a course on operating systems. Typically, these students study concepts, structure and mechanisms of operating systems using one of the many good textbooks that are available (Tanenbaum, Stallings, Nutt, Silberschatz & Galvin,..). All these textbooks contain one or more chapters on principles of concurrency, which discuss fundamental concepts such as mutual exclusion algorithms, sempahores, monitors, message passing, deadlock and starvation. The concepts are introduced informally: the authors do not want to bother their readers with formal correctness proofs since this would distract attention from the key issues they want to get accross. Correctness proofs of of the algorithms is typically left as an exercise and there is no mentioning of formal methods or model checking.
We think that after 20 years of research on model checking this technology has become sufficiently mature and it is time to change the way in which we teach principles of concurrency:
- Using the input language of model checkers it is straightforward to formalize concurrency algorithms in terms of networks of communicating state machines. If we explain concurrency algorithms then it is often better to use pseudo code or text rather than logical formulas. However, it greatly help to understand things when they know how the pseudo code and text correspond to precise mathematical models and assertions about these models. By specifying state transitions, we make made explicit which operations are atomic and which operations are not, an issue that is vital to understanding the algorithms.
- Using the (graphical) simulators provided by some modern model checkers such as Uppaal, it becomes very easy to visualize the behavior of concurrency algorithms and certain problematic traces in which mutual exclusion is violated, starvation occurs, etc.
- Using the model checker students can convince themselves of the correctness of algorithms without having to spend a lot of effort on tedious, manual correctness proofs (which are of independent interest but belong in a course on program correctness rather than in a course on operating systems).
The goal of this project is to advance the use of model checkers in education by
- Building a website with an extensive repository of solutions via model checkers of basic concurrency problems.
Improving model checkers (in particular Uppaal) to make them more suitable for this type of examples.
- Developing course material.
For more information see here.
Project 4: Analysis of Wireless Sensor Networks
A small and dedicated group of Dutch companies have joined forces to develop a substantial experimental wireless sensor network in the Netherlands. The aim of this project is to be a technology showcase for the participating companies and a breeding ground for both business development and relevant academic research. This initiative is called MyriaNed. The MyriaNed project is of interest first of all because the sheer size of the network (at least 10.000 nodes) will challenge current state-of-the art analyses techniques, but also because the MyriaNed project has a lifetime sufficiently long to support a PhD project. The MyriaNed node prototypes have been developed in 2006 and they are already available for experiments. A small scale trial is currently deployed in Rotterdam consisting of 20 nodes. Given the limited functionality CPU and radio frequence communication, power usage is a major design driver because these devices will, in principle, be battery operated. This basic MyriaNed infrastructure (the wireless sensor network) has to be aligned with the application it is going to support. This application has certain dependability requirements that must be satisfied by the MyriaNed architecture. Potential research questions are (but not limited too):
- w.r.t. reliability, e.g.: Is it possible to prove that information is always eventually delivered? What is the average time to deliver such a message?
- w.r.t. usability, e.g.: How does the communication demand from the application affect the power usage of a single node and the network?
We intend to tackle these problems using real-time and probabilistic model checkers. Without exception, all these example problems are challenging in terms of both modeling and analysis, in particular taking the scale of the network into account. Attempts to use simulation tools to characterize these questions often fail because they do not scale up or do not cover the corner cases suffciently to provide realistic results.
This research will be carried out in close collaboration with the Dutch Company Chess.