Motivation

1. IT Systems
A large fraction of contemporary Information Technology systems are either

• Embedded Systems offering autonomous and intelligent control of complex physical systems, or
• Service Oriented Architectures providing services designed to support machine to machine interaction over a network.

Cutting edge examples include intelligent vehicles that actively prevent accidents, intelligent homes that automatically adapt to your lifestyle, and services for handling electronic shopping and secure payments. On a larger scale the future integration of medical equipment, electronic hospital records and next generation communication technologies are examples pointing towards the trend of service oriented systems incorporating a number of embedded components.

2. Properties
The stability of the IT infrastructure of our future society demands that a number of fundamental properties can be validated for the IT systems of interest. This spans properties related to safety and security (e.g. ‘no virus can allow outsiders to get access to my net bank’), to performance (e.g. ‘my critical internet service will be available 99.99% of the time’) and to resource usage (e.g. ‘the control system rotates and adjusts the windmill such that at least 60% of the potential wind energy is utilised’).

a. The Challenge
Due to their interaction with the surrounding, physical environment, the modelling and validation of embedded and service oriented systems must include discrete (e.g. providing safety and security guarantees), stochastic (e.g. dealing with performance) as well as continuous aspects (e.g. providing measurements of resource usage). A shift in paradigm is required in the development of IT systems from the study of discrete properties to also include stochastic and continuous properties.

MT-LAB will develop a new foundation of Computer Science by integrating discrete, stochastic, and continuous properties of future IT systems.

Example challenges include:

1. Intelligent houses of the future exhibit a clear need for hybrid modelling. Here sensors will monitor continuous parameters like temperature, humidity, and air quality, while control programs adjust the indoor conditions to optimal comfort by commanding pumps, heater switches, electric windows and ventilators. Simultaneously fire and burglar alarms are always ready to quickly alarm both the security company and your mobile phone.
2. In the future it will be possible to treat patients at home. This is both more attractive for patients, and cheaper for hospitals, but requires development of an intelligent health care infrastructure comprising, e.g., automatic medicine dispensers and blood test collectors. Such applications impose much higher correctness and security requirements than typical IT systems of today.
3. The introduction of the Danish electronic payment system with chip cards has been notoriously painful. From the traditional data security point of view the system was satisfactory, but its long response times have hindered its deployment in practice. One of the reasons was that the IT industry's development tools are largely incapable of taking stochastic properties into account, so problems with quantities, like response time, are discovered late.

These examples indicate that the upcoming IT systems, because of their relation to the environment, will turn out to be much more complicated than the IT systems we use today. Consequently it will no longer be possible to study the IT systems on their own premises, but they should be analyzed together with the physical components, with which they interact.

b. Meeting the Challenge
To achieve this revision of Computer Science we will develop powerful computational methods and algorithms for the analysis of discrete, stochastic and continuous properties. To obtain valuable feed-back on the appropriateness of the development we will test our methods on well chosen examples using prototypes developed or refined within the project.

In order to stimulate the interaction between the complementary competences of the researchers we find it useful to employ a "matrix-structure" for clarifying our research tasks. Here one dimension corresponds to the models and properties studied:

• discrete, e.g. providing safety and security guarantees,
• stochastic, e.g. dealing with performance, and
• continuous, e.g. providing measurements of resource usage.

The other dimension is designed to highlight the complementary competences of the researchers and will be explained in detail later; here we just give a brief overview:

1. Static analysis and model checking are complementary approaches to the validation of discrete and, to a certain extent, stochastic and continuous systems.
2. Embedded systems and service-oriented architectures are two dominant platforms for the development of IT systems – they are expected to merge and create the IT systems of future.
3. Components and characteristic features are complementary approaches to the construction and understanding of complex IT systems.