Models and Logics for Quantitative Analysis

A proposal for an ERCIM Working Group

 

This is a proposal for establishing an ERCIM Working Group called MLQA on Models and Logics for Quantitative Analysis.

 

Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will

(1)  consider process models formally described by transition systems, automata or process calculi,

(2)  we will consider logics for expressing stochastic and continuous properties as well as discrete ones,

(3)  we will focus on algorithms, theory and tools, and

(4)  we will study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.

 

The MLQA home page: http://www.MT-LAB.dk/MLQA 

1. 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.

2. 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

 

 

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.

 

3. ERCIM Working Group

ERCIM - the European Research Consortium for Informatics and Mathematics - aims to foster collaborative work within the European research community and to increase co-operation with European industry. Leading research institutes from nineteen European countries are members of ERCIM and for this reason ERCIM is seen as a natural host of the proposed working group. Please consult www.ercim.org for more information about ERCIM.

 

It is also believed that the clear focus on models and logics within discrete, stochastic and continuous properties helps to separate the working group from existing ERCIM working groups on Formal Methods for Industrial Critical Systems and Dependable Software-intensive Embedded Systems. On the one hand, we believe that our more narrow focus on models and logics will be effective in fostering new synergies between existing research groups. On the other hand, we believe that our wider focus on application areas beyond those of traditional IT systems falls well outside existing ERCIM working groups on formal methods.

4. Proposing Institutions

At present the following institutions, that are members of the national organisations taking part in ERCIM, support the proposed MLQA working group (in alphabetical order and just one contact person per site):

 

á      CNR (Italy) / Diego Latella

á      CWI (Holland) / Jan Rutten

á      INRIA (France) / Catuscia Palamidessi

á      Oxford University (England) / Marta Kwiatkowska

á      RWTH Aachen University (Germany) / Joost-Pieter Katoen

á      Technical University of Berlin (Germany) / Uwe Nestmann

á      Technical University of Denmark / Flemming Nielson

á      Trinity College (Ireland) / Matthew Hennessy

á      UniversitaÕ di Firenze (Italy) / Rocco De Nicola

á      University of Trento (Italy) / Paola Quaglia

á      University of Edinburgh (Scotland) / Stephen Gilmore

á      UniversitŠt des Saarlandes (Germany) / Holger Hermanns

á      University of Aalborg (Denmark) / Kim Guldstrand Larsen

4. Objectives

The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.

 

To reach these goals a number of activities are foreseen:

á      An annual meeting (for 2009 the Kick-Off meeting, for 2010 a meeting at a major conference or an international meeting facility such as Dagstuhl, for 2011 colocation with a relevant cluster of conferences like QEST and CONCUR in Aachen).

á      Formulating a research programme – that can influence activities at participating institutions and that might lead to the formulation of an European project or network on formal quantitative analysis.

á      Exploiting current funding possibilities (ERCIM fellowships, Marie Curie stipends, etc.) to support the mobility of (young and prospective) researchers.

á      A web page with information about activities, tools, and opportunities.

á      Possibly to produce a book covering state of the art in the area. This should consist of tutorials and survey papers on key components and there should be an attempt at putting them into perspective for the wider aims of the working group. Depending on the interest of the working group members a target time frame might be as early as 2011.

 

Once created, the working group will be open also to researchers outside of ERCIM (and outside of Europe).

5. Revision Structure

á      Originally drafted by Flemming Nielson in August 2008 (borrowing from www.MT-LAB.dk) with comments from Matthew Hennessy and Diego Latella and discussions with a group of proposers.

á      Revised in April 2009 by Flemming Nielson with help from Stephen Gilmore and Diego Latella and taking note of the discussion at the Kick-Off meeting on March 28, 2009 (as part of ETAPS in York) and the subsequent discussions.

á      Revised May 2009 after comments from the mailing list members.

6. Contact Person

Professor Flemming Nielson, DTU Informatics, nielson@imm.dtu.dk