Model Based System Development/Move or Clean UP/Research Programme

ITA Research Programme

Our long term research objective is to give the discipline of computer-based system engineering a sound mathematical basis via the development of appropriate semantic models, powerful model checking and verification techniques, and good methods for formal specification and development. As a source of inspiration and in order to ensure the applicability of our approach, we tackle challenging case studies from the area of embedded systems and distributed algorithms and protocols. Much of our work takes place within externally financed projects:

• Our work on semantic modelling frameworks for real-time, hybrid and probabilistic systems takes place mainly in the context of the IST project Ametist and the DFG/NWO collaboration project VOSS2.
• Our work on model checking real-time systems is carried out within Ametist. The overall goal of Ametist is to initiate the development of an emerging discipline: computer-aided timing analysis and design. We expect that the distinction between model-checking and interactive theorem proving will become less strict; more user-guidance will enter the model-checking activities, and the level of automation of theorem provers will be increased by introducing suitable strategies.
• Our work on testing takes place in the context of the EZ/Senter project TANGRAM and the NWO/EW project STRESS.
• Our semantic frameworks and analysis tools are applied for the formal specification and development of embedded systems. Within the Boderc project of the Embedded Systems Institute, we intend to integrate UML-based software design for embedded systems into a common framework that is suitable for multi-disciplinary system engineering. This involves hybrid modeling, architectural descriptions and high-level analysis based on formal methods and tools. An Oce printer is taken as a case-study and acts as a driver for this project.
• Another area where we apply our semantic frameworks and analysis tools is analysis of distributed algorithms and network protocols. Within the NWO project FRAAI we investigate an incremental approach to develop fault-tolerant real-time protocols.

In addition, research is carried out on the following topics:

• methodology
• image processing