http://www.dagstuhl.de/15504

06. – 09. Dezember 2015, GI-Dagstuhl Seminar 15504

Formal Evaluation of Critical Infrastructures

Organisatoren

Erika Abraham (RWTH Aachen, DE)
Anne Remke (Universität Münster, DE)
Markus Siegle (Universität der Bundeswehr – München, DE)
Marielle Stoelinga (University of Twente, NL)

Auskunft zu diesem GI-Dagstuhl Seminar erteilt

Heike Clemens

Dokumente

Seminar Schedule [pdf]

Motivation

Our society vitally depends on the reliable functioning of critical infrastructures: most prominently the electrical power grid, water and gas distribution networks, as well as the associated information and communication systems. These systems need to work reliably 24 / 7 and failures can be extremely costly or even threatening for both economy and society. It is of utmost importance that such critical infrastructures survive catastrophic events, but they are becoming increasingly complex and interconnected and therefore more vulnerable to failures, natural disasters and attacks. This renders the development of dependable critical infrastructures a major challenge.

This seminar advocates the use of formal methods with a strong emphasis on the quantitative (as opposed to only qualitative)model-based evaluation of critical infrastructures. Formal methods provide a rigorous framework for specifying and verifying systems, involving the construction of models from high-level descriptions and enabling analysis of all possible behaviours, including best- and worst-case scenarios. The technical goal of this seminar is to adequately model the interplay between discrete and continuous phenomena, which appear in critical infrastructures. Randomized hybrid models, offering both discrete and continuous state components, appear as a natural choice to accurately model critical infrastructures. There have been recent advances in modelling and analysing randomized hybrid systems, however, available algorithms are not yet applicable to the special requirements of critical infrastructures. In order to adequately model critical infrastructures, an innovative combination of different formalisms and techniques are needed to describe the various components of a system as well as their interdependencies.

Scientific program

In the tradition of the DFG/NWO-supported Dutch-German Bilateral Cooperation Program ROCKS (http://www.rocks-project.eu/), in which all organizers were involved and which was successfully completed 2013, our aim is to offer a platform for gifted young scientists at all educational levels to explore an interesting and challenging scientific field, exchange ideas and scientific results, initiate cooperations, and profit from the networking with senior scientists.

To reach this goal, the will follow a twofold approach, presenting published and on-going work on quantitative evaluation and recent extensions towards randomized hybrid models, but it will also leave room for discussing possible future extensions and collaborations with respect to the development of methods for the compositional formal analysis of the desired quantitative measures. The program of the seminar will evolve around the following three topics:

  1. Modelling languages: From engineering standards via automatic model transformations to evaluation formalisms, covering both probabilistic and hybrid aspects with a focus on compositional modelling. This involves novel modelling techniques, e.g. probabilistic hybrid automata or stochastic differential equations, as well as combinations of such formalisms. We will identify the main modelling characteristics of the different applications in critical infrastructures and start to develop predictive models, which correctly describe critical infrastructures and their interdependencies. These models will combine stochastic elements with hybrid aspects and real-time. We will investigate specialised failure models that take into account the interactions within and between distributed critical infrastructures, with phenomena such as failure propagation, cascading failures and escalating failures.
  2. Model checking algorithms: Rigorous formal analysis techniques for the quantitative evaluation of large randomized hybrid models, where scalability by means of compositionality is a key issue. Recent algorithms are based on principles such as abstraction / refinement and rely on sophisticated data structures and coding strategies which are crucial for efficiency. We will investigate how these methods can be used to analyze the dependability, survivability and resilience of critical infrastructures, to analyze the evolution of the models, and to quantify effects of failures and the cost of outages and recovery processes.
  3. Parameter synthesis and controller synthesis: Finding parameter values and control strategies such that the considered critical infrastructure will meet its specification even in an adverse and unpredictable environment.

Organisation

This seminar will bring together junior and senior researchers from the area of quantitative modeling and verification of hybrid systems with those from critical infrastructures, which is an optimal setting for a fruitful collaboration and will serve for the training of young scientists who want to acquire essential qualifications and skills.

We will have an open application procedure for PhD students and Postdocs, who are invited to send a motivation letter. We will also invite experts on the different fields to ensure a good mixture between senior and junior researchers. The schedule of the seminar will consist of invited lectures from senior researchers, as well as shorter presentations from junior researchers and will leave room for collaboration and discussions.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact aufgelistet und separat in der Bibliothek präsentiert.