Distributed algorithms and protocols have become of vital importance for consumer electronics. Over the last years there has been an enormous effort by the industry to develop various protocol stacks, such as IEEE 1394 'Firewire' and HAVi, and to incorporate these into consumer products. Even though these products are mostly not safety-critical, the financial implications of errors or bad performance can be enormous, simply because of their mass replication. This implies that the verification of the correctness of such systems is of great practical importance. The very high complexity of the protocol stacks, however (specifications typically take up several hundreds of pages), turn their verification into a major challenge. In addition to the problems of size, the analysis of the time dependent features is an important source of problems because of the rather subtle complications that they may cause. This project aims at the development and integration of methods and tools for the verification and analysis of real-time embedded systems, with an emphasis on distributed algorithms and protocols for consumer electronics applications. The goal is to consider not only 'hard' real-time constraints (e.g. the system must always do x before a given time) but also so-called 'soft' real-time constraints (e.g. the system should usually do x before a certain time). For the last type of constraints we will take a stochastic point of view. Many systems combine different sorts of features, with often purely functional behaviour in large parts and a small number of additional hard/soft real-time requirements in one or more specific places. It has clear advantages to offer means for the verification of such different properties in a single framework, and the project, therefore, aims at an integrated approach of the verification problem. A clear theoretical and practical link is sought to both purely functional analysis on the one hand, and the area of performance analysis on the other.
Concretely, the project has the following objectives:
Our project builds directly on the experience and results of two joint research projects that are to be completed in 1999, and justify our expectations that the above project goals are indeed realistic. The SION project "Testing and Verification of Timed Systems (TVTS)" (KUN, UT) has produced significant theoretical results as well as a prototype tool (SPADES) that to a large extent provide the basis for the present project. The results obtained (testing theory for timed systems, process algebra of timed and stochastic systems) must now be used to obtain workable verification methods for hard and softly timed systems. The SPADES tool can be used as the starting point for more serious tool development.
The other preceding collaborative project (CWI, UT, (KUN, and Philips Research) is "Specification, Testing and Verification of Software for Technical Applications (STVSTA)". In this project a number of protocols within the IEEE 1394 and HAVi stacks have been analyzed successfully, using a combination of methods and tools for verification and testing (LOTOS, SPIN, Caesar/Aldebaran, I/O automata, PHACT,..). The project has given us considerable experience in dealing with correctness issues in an industrial setting, restricted however to functional and hard real-time correctness properties only. Clearly, studying soft real-time properties and performance analysis would also be of great importance for these protocols. To ensure the practical relevance of the case studies of this project, the highly successful and productive format of the STVSTA project will be adopted. It is thus envisaged that a PhD will carry out the case studies in close cooperation with Philips Research. They involve some 5 different application cases of about half a year's work each.
October 1, 2002