Research Topics

Non-Technical Mission Statement

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 web services designed to support Machine to Machine interaction over a network). This tendency will greatly increase in what is going to become the Internet of the Future, an integrated system comprising telecommunication, the internet, and small systems embedded in domestic applicances. Cutting edge examples include intelligent vehicles that actively prevent accidents, intelligent homes that actively support your lifestyle, and services for handling electronic shopping and secure payments. On a larger scale the future integration of medical equipment, emergency support systems, electronic hospital records and next generation communication technologies are examples pointing towards the trend of Service Oriented Systems incorporating a number of Embedded Components. On an even larger scale, we begin to see IT Guided Workflow Systems where the human activities are mainly those of domain experts (e.g. a doctor who is an expert in a given treatment) rather than being in charge of the overall workflow (e.g. monitoring the treatment history from the point of view of the patient). Going outside of the traditional domains of IT Systems there is a growing use of computer science modelling and analysis techniques also within Life Sciences, in particular the modelling of components of Biological Systems.

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 security (e.g. ‘no virus can allow outsiders to get access to my internet bank’), to performance / dependability (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’). Even the formulation of these properties become non-trivial when addressing IT Guided Workflow Systems that have humans as ‘subsystems’ and when addressing description of the three dimensional behaviour of Biological Systems.

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 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 – not least when addressing IT Guided Workflow Systems. The use of stochastic and continuous properties is equally important in the domain of Life Sciences.

Objectives. To meet the above challenge we need powerful modelling methods and algorithms for the analysis of discrete, stochastic and continuous properties. The aim of this working group is to create a venue for knowledge sharing in this exciting area and creating a network also for young researchers; furthermore for sharing tools for performing analyses and for creating joint European research projects on quantitative analysis.

Technical Mission Statement

Models of IT Systems. The construction of IT Systems spans a large number of abstraction levels ranging from low-level, hardware-oriented programming languages (e.g. VHDL), high-level programming languages (e.g. C++ and Java) to object-oriented development notations (e.g. UML).

To ensure applicability at all levels and independence of concrete programming languages, we will focus on modelling system behaviour by means of process models expressed using process calculi, transition systems or automata. These models are able to model a wide variety of discrete and stochastic features whereas further development is needed to fully account for the continuous ones. The study of open systems is well studied but needs to be extended to the study of IT Guided Systems where the human components cannot be fully described and to the description of Biological Systems where components need to be understood in three dimensions.

Specifications of Properties. To ensure the quality of systems, the Safety Instrumented Systems standard is pervasive in the area of embedded systems, and the Common Criteria standard is widely used in many NATO countries; they are examples of international standards that emphasize the need for validating that systems are

• functionally correct (react as expected),
• safe (do not cause damage on environment or users),
• highly efficient while demanding few resources,
• secure (against hackers and viruses),
• stable (do not crash),
• fault tolerant (offers vital functionality even when partially crashed).

To ensure a uniform approach to studying these important properties, we will be based on logical specification formalisms that are able to accommodate seemingly dissimilar properties within the same formalism and that facilitate the construction of automatic validation engines. These formalisms are able to express all discrete properties and a good selection of stochastic and continuous ones. They have been used widely as part of analysing Embedded Systems and Service Oriented Architectures but may need to be developed further to fully deal with IT Guided Workflow Systems and Biological Systems.

The Challenge. While more work is needed to ensure that models and specifications can express the phenomena of interest, the main challenge is in providing the effective methods, techniques and algorithms that allow the models of IT Systems to be verified against the specifications of properties. New challenges may arise from the study of IT Guided Systems where human components by their very nature cannot be fully described and when describing the multi-dimensional nature of Biological Systems.

We now take a closer look at state-of-the-art and challenges within each of the discrete, stochastic and continuous dimensions.

Discrete Models and Properties. The Computer Science approach to IT Systems is traditionally based on discrete models that consciously abstract away from less relevant physical phenomena, e.g., the discrete model of a finite automaton is often a useful abstraction of an electronic device. Static analysis and model checking are two of the most prominent techniques for discrete systems analysis. In many ways they are complementary and largely developed by independent research communities. In 2007 the Turing Award was given to Clarke, Emerson and Sifakis for their work on model checking. The techniques are used by some of the largest international companies (e.g. IBM, Intel, Microsoft). A related technique is that of theorem proving that may provide less automation but is often able to deal with stronger properties.

The scientists involved in the working group are reputed for their contributions within these areas, and want to exploit this unique position in creating new combined analysis techniques more powerful than seen before.

Stochastic Models and Properties. The quantitative properties of the environment of a given IT System are often accompanied by uncertainties best described using stochastic or probabilistic models, as for example Markov Chains, Markov Decision Processes, and Continuous Time Markov Decision Processes. Probabilistic and stochastic process models have been subject to significant research during the last 10-15 years, with an exciting development towards the modelling of Biological Systems starting some 5-10 years ago.

Within a number of European projects the scientists involved in the working group have contributed significantly to model checking methods for different types of Markov models (Discrete / Continuous Time Markov Chains, Markov Decision Processes). The working group will focus on extensions to models combining stochastic and continuous aspects and will develop – so far non-existing – static analysis techniques applicable to stochastic models.

From the point of view of “traditional” mathematical modelling the working group offers a unique chance to integrate and further develop recent advances in stochastic models. This involves techniques for dealing with the joint distribution of distinct properties of interest. An important example would be the joint distribution of the time and energy required to complete a certain task.

Continuous Models and Properties. Within classical Control Theory the predominant way of modelling an IT System is through a set of differential equations describing the evolution of physical phenomena in the environment when regulated by a given control program. A serious restriction is that only systems with completely deterministic behaviour may be modelled, making it impossible to handle distribution of computation. To overcome this restriction, the new area of Hybrid Systems has emerged in the intersection between Computer Science and Control Theory.

The scientists involved in the working group will concentrate on the challenge of defining property preserving transformations from hybrid system models to discrete models in order that the powerful analysis techniques for discrete systems may be applied. Also we will devote effort to defining – so far mainly absent – logical specification formalisms and analysis methods.

From the point of view of “traditional” mathematical modelling the approach offers a unique chance to develop tractable ways of dealing with important control system properties, such as reachability (ability of a system to attain a specified goal) and stability (ability to keep the goal against disturbances), which is currently beyond state-of-the-art. A challenging crosscutting combination of stochastic and mathematical models is the study of stochastic differential equations, an area known as Stochastic Control Theory. Here the challenge is to find an adequate stochastic process, which realistically models the uncertainty inherent in the given problem, and to develop the corresponding algorithms.