Seminar Description

More and more, our society and economy rely on the well-operation of, often hidden, Information and Communication Technology Infrastructures. These infrastructures play an ever-increasing role in other Critical Infrastructures, such as the power grid and water and gas distribution networks. Such systems are highly dynamic and include assets that are essential for the functioning of our society and economy. Users need to be able to place a high level of trust in the operation of such systems, however, uncertainty in the environment, security and physical attacks, and errors in physical devices pose a serious threat to their reliable operation. Hence, it is very important that Critical Infrastructures survive catastrophic events.

Hence, modeling Critical Infrastructures and developing methods to analyze their safety and dependability, in the presence of failures and disasters is of utmost importance. It is of special interest to analyze, how quickly systems recover to acceptable levels of service after the occurrence of disasters, the so-called survivability. However, both failure and repair processes are random and a probability distribution is needed to describe how they evolve over time.

Randomized Timed Models are able to take the dependency of such processes on time into account and powerful techniques exist for their analysis. However, for Critical Infrastructures a modeling formalism is needed that allows describing both discrete and continuous quantities. Examples of discrete quantities are the number of spare parts and the state of sensors, actuators and Information and Communication Technology components, whereas the physical quantities, like the amount of produced energy or the quality of the treated water in terms of temperature and pressure naturally constitute continuous quantities.

Randomized Hybrid Models have been successfully applied to model safety-critical applications. Due to the flexible combination of discrete and continuous state components, Randomized Hybrid Models appear as a natural choice to accurately model Critical Infrastructures. Some formalisms were proposed for the analysis of Randomized Hybrid Models, and an increasing interest and activity can be observed in this field. Still, the industrial application that we are considering is far too large for state-of-the-art approaches; either they are applicable to specific applications only or they do not scale.

Up till now, most modeling in Critical Infrastructures is still fairly "classical" using reliability block diagrams, fault-trees or simplistic stochastic Petri nets. While researchers from the Critical Infrastructures community could benefit from recent advances for Randomized Hybrid Models and their formal analysis, existing algorithms are not yet readily applicable to the special kind of problems arising in Critical Infrastructures.

This clearly shows the need for bringing together experts in the areas of Randomized Timed Models and Randomized Hybrid Models with those from Critical Infrastructures. In the following we describe interesting advances in all three fields and comment on how they can help to bridge the current gap between the fields.

Critical Infrastructures

Critical Infrastructures are in general controlled by SCADA (supervisory control and data analysis) systems, which are potentially vulnerable to attacks and misuse. SCADA systems consist of sensors, actuators, controllers and a human-machine interface through which human operators control the physical process. It is important to correctly capture interdependencies that arise between the SCADA network and the physical network, but also interdependencies between different Critical Infrastructures.

The complex nature of Critical Infrastructures requires a flexible and scalable compositional modeling framework that is able to accommodate different levels of abstraction. At design time, usually not all parameters and not all usage patterns are known exactly. Also the specific details of vulnerabilities and failures might be unknown, such as the mean time to failure and the impact of a given vulnerability. In such cases it is appropriate to make stochastic assumptions about the system and the disaster behavior.

The heterogeneity of typical Critical Infrastructures may require a combination of different formalisms and techniques to describe the various components of a system and their dependencies. For example, the combination of continuous and discrete phenomena may need to be captured in the modeling framework, e.g, to model the process automation and the production process which is the essential part of several Critical Infrastructures.

Interactions and dependencies between subsystems of different nature inside a Critical Infrastructure or among cooperating Critical Infrastructures require advanced methods to reconcile different aspects under a common development and assessment framework. Compositional modeling can simplify the modeling process and can lead to intuitive formalisms. Furthermore, it enables compositional analysis techniques, which might reduce the complexity of verification and build a challenging topic that requires additional research.

In the seminar we discussed questions like the following:

• Which modeling methods are suitable for which types of Critical Infrastructures?
• Which are the crucial system issues that must be considered when accurately modeling Critical Infrastructures?
• How to distinguish the crucial parameters, thereby keeping the state space of the models as small as possible?

Randomized Timed Models

Randomized Timed Models have been widely used for the modeling and evaluation of, e.g., computer and communication systems. They are in general well understood, suited to model complex systems, and efficient methods and tools exist for their analysis and simulation. Different modeling formalisms differ, e.g., in the model of time (discrete or continuous), in the existence or absence of nondeterminism, or the support of rewards.

Discrete-Time Markov Chains (DTMCs) belong to the most basic probabilistic models, offering a discretized model of time in the absence of nondeterminism. Continuous-Time Markov Chains (CTMCs) extend DTMCs by a continuous model of time. Several temporal logics were extended to specify relevant properties of Randomized Timed Models, and model checking algorithms were developed to check their validity for the above models. For example, Probabilistic CTL (PCTL) properties for DTMCs can be checked efficiently by solving systems of linear equations. Furthermore, efficient computation algorithms have been developed for model checking Continuous Stochastic Logic (CSL) properties of CTMCs (Baier, Haverkort, Hermanns, Katoen, 2003).

High-level formalisms like General Stochastic Petri Nets (GSPNs) and Stochastic Activity Networks allow to describe complex systems in a more compact way. Their evaluation can be lead back to methods for Markov chains.

Failure and repair processes of Critical Infrastructures often exhibit nondeterminism. Markov Decision Processes (MDPs) and Continuous-Time Markov Decision Processes (CTMDPs) extend DTMCs respectively CTMCs with the notion of nondeterminism. These powerful models can be analyzed by determining an optimal scheduler that removes the nondeterminism from the system and allows to apply the model checking approaches for DTMCs and CTMCs. Algorithms exist that compute such optimal schedulers based on solving the underlying optimization problems.

The non-functioning of Critical Infrastructures easily results in huge economic losses. To model the costs of failure and repair, a notion of reward can be added to the above models, resulting in so-called Markov Reward Models (MRMs). To specify properties related to rewards, CSL has been extended to Continuous Stochastic Reward Logic (CSRL). Adding rewards to Randomized Timed Models makes the model checking problem very challenging. However, numerical algorithms exist for, e.g., model checking CSRL properties with arbitrary time and reward intervals for CTMCs with rewards. This is extremely useful for Critical Infrastructures, since these algorithms provide a direct and precise method for model checking survivability properties (Cloth, Haverkort, 2005).

There is quite a number of tools available for the analysis of the above model types. The most prominent ones are PRISM, MRMC, Möbius, Smart, CADP, or LiQuor. Besides formal verification, there are also simulation-based tools (e.g., APMC, VESTA). Most of these tools were successfully applied to different industrial case studies. However, these formalisms and tools are only partially suited for the model checking of Critical Infrastructures, mainly due to the lack of scalability and modeling power.

Model checking for the above models suffers from the well-known state explosion problem when applied to highly complex and large models of Critical Infrastructures. This problem could be tackled by compositional modeling and verification. However, though the models themselves support compositionality, there are no methods and tools readily available for compositional verification. Moreover, all the above models lack the power to model continuous physical processes, which is an essential part of Critical Infrastructures. Hence, the following section focuses on Randomized Hybrid Models.

In the seminar we discussed questions like the following:

• What are the (dis)advantages of the different modeling formalisms available?
• Which properties of Critical Infrastructures can already be efficiently analyzed with existing techniques?
• What are the requirements for compositional modeling and verification?

Randomized Hybrid Models

When adding continuous behavior to discrete systems, the hybrid models become very powerful and in general undecidable. The most popular modeling formalism for hybrid systems are Hybrid Automata. Several analysis techniques were proposed for their reachability analysis, based on, e.g., approximation, hybridization, linearization, the usage of theorem provers, and interval-arithmetic.

Different approaches exist to extend hybrid models with randomized behavior. The most important difference between the extensions is where randomness is introduced. Timed Automata and Hybrid Automata were extended with probabilistic discrete jumps (in the style of DTMCs and MDPs) to Probabilistic Timed Automata respectively Probabilistic Hybrid Automata. In contrast to probabilistic discrete jumps, other formalisms, e.g., Piecewise Deterministic Markov Processes (Davis, 1993), allow initialized jumps to take place at random times (in the style of CTMCs and CTMDPs).

An orthogonal extension lies in introducing stochastic differential equations for modeling perturbations in the dynamic time behavior. When combined with probabilistic discrete jumps, this yields the model of Stochastic Hybrid Systems (Hu, Lygeros, Sastry, 2000). Another possibility considers the combination with CTMC-style stochastic jumps resulting in Switching Diffusion Processes (Gosh, Araposthatis, Marcus, 1997).

Only some simple classes of these models are decidable; their analysis can be lead back to the analysis of corresponding decidable classes of Hybrid Automata (Sproston, 2000). Despite the undecidability of the above general classes, there are incomplete approaches available for their analysis, based on, e.g., Markov Chain approximation (Prandini, Hu, 2006) or discrete approximation (Koutsoukos, Riley, 2008). Latest work considers CEGAR-style abstraction that allows the application of model checking methods for Hybrid Automata (Zhang, She, Ratschan, Hermanns, Hahn, 2010).

Also the high-level Petri Net models can be extended with hybrid and randomized behavior. Including a notion of time, as in Timed Automata, results in Timed Petri Nets. Hybrid Petri Nets (David, Alla, 2001) are a high-level formalism for general Hybrid Automata. Colored Petri Nets correspond to Piecewise Deterministic Markov Processes (Everdij, Blom, 2009), supporting initialized stochastic jumps. Fluid Stochastic Petri Nets can be seen as a generalization of Piecewise Deterministic Markov Processes, allowing for jumps to take place after a negative exponentially distributed amount of time. Besides the stochastic jumps, these models resolve nondeterminism by introducing discrete probability distributions for concurrently enabled transitions. This way, these models support both a probabilistic choice of jumps and a stochastic randomization of the time point of jumps, making the models extremely expressive and hard to formally analyze. Fluid Stochastic Petri nets can be solved analytically for up to three fluid places. For more general classes, simulation has to be used.

This variety illustrates the emerging interest of the research community in Stochastic and Probabilistic Hybrid Models. Traditionally, academic research focuses stronger on decidable subclasses than on efficient algorithms applicable to more expressive models. However, especially for Critical Infrastructures, models are needed that are able to specify complex continuous dynamics, e.g, in order to study recoverability processes.

For more expressive hybrid models, available analysis methods apply techniques like simulation, dynamic programming, and approximation. The Critical Infrastructures community would strongly benefit from the developments of modern model checking algorithms for models combining randomized and hybrid behavior.

In the seminar we discussed questions like the following:

• What particular hybrid model classes are suitable for Critical Infrastructures?
• How can initialized models be evaluated?
• How can efficient analysis (especially model checking) techniques be adapted for Randomized Hybrid Models?

Achievements of the Research Seminar

This seminar offered a platform to bring together researchers, both from academia and industry, working on Randomized Timed Models, Randomized Hybrid Models and Critical Infrastructures. The program of the seminar was a balanced combination of (i) tutorials and presentations from all three fields to motivate collaboration and to develop a common ground for discussions and (ii) time for collaboration, where actual progress is expected to be made on increasing the efficiency, applicability and application of formal modeling and analysis techniques for Critical Infrastructures.

More specifically, we feel that this seminar helped to improve the development in the given area in the following points:

1. The seminar increased the interest for both the academic development and the industrial application of formal methods to Critical Infrastructures and draw attention to open issues. We discussed industrially relevant case studies and specific requirements on modeling formalisms and evaluation techniques in this context.
2. While most of the existing work on Critical Infrastructures focuses on simulation, this seminar aimed at a thorough discussion of the requirements for appropriate formal analysis techniques. We provided an overview of the modeling and analysis methods already available in Randomized Timed and Hybrid Models, including a thorough discussion of their suitability for Critical Infrastructures.
3. We initiated discussions and cooperations that advance the state-of-the-art in Critical Infrastructures, regarding both the development and the application of suitable modeling formalisms and analysis techniques for Critical Infrastructures. We offered a platform to join expertise from different fields, to exchange knowledge about existing methods and applications, to push forward the communication of needs and interests, and to draw attention to challenging research fields and promising applications in the area of Critical Infrastructures.

Creative Commons BY 3.0 Unported license

Erika Abraham, Alberto Avritzer, Anne Remke, and William H. Sanders