University of Twente (THE NETHERLANDS)
Input/Output Interactive Markov Chains
CADP (Construction and Analysis of Distributed Processes)
35,330 states and 405,112 transitions
Water cleaning and distribution has been identified as one of the
critical infrastructures. They all include assets that are essential
for the functioning of a society and economy. Hence, it is very
important that critical infrastructures survive catastrophic events.
A water treatment facility cleans raw water in approximately fifteen
steps before the water is distributed to households and companies.
In case the facility fails to provide clean water it will be charged
high fines by the companies it is supposed to deliver to, and it will
suffer damage to its public image.
This work focuses on the distribution station of a water treatment facility, for which availability (readiness for correct service), reliability (continuity of correct service), and survivability (ability to recover), are analyzed. The distribution part of a water treatment facility is modeled in Arcade by creating basic components (BCs) for the valves and the tank. A valve can fail in two ways, it can either be stuck closed or open. A tank can fail because of several reasons, it can rupture, be contaminated or leak. It is assumed that the pipes do not fail, and therefore they are not modeled. For simplicity, every BC has its own repair unit (RU). By composing the RUs with the corresponding BCs, general Input/Output Interactive Markov Chains (I/O-IMCs) are obtained for a valve and the tank.
The analysis is carried out in several steps: using a fault tree expressing the need for two water districts to both receive water, the I/O-IMC is first converted into a Continuous-Time Markov Chain (CTMC) using Arcade; the fail and up transitions that indicate the state of the entire system are hidden; all internal transitions present in the Arcade model are removed using the REDUCTOR tool of CADP; finally, the stochastic MRMC model checker is used for analyzing the resulting CTMC.
A CTMC of the water distribution station was created and analyzed for
availability and reliability. Furthermore, the model was adapted to
make possible the survivability analysis. The model obtained is
estimated to be correct, since the survivability measures predicted
by model checking were exactly the same as those for a manually created
CTMC of the distribution station.
Future work includes a more comprehensive analysis of the water distribution station, that involves in particular the computation of quantitative properties. For instance, rather than computing the survivability as the probability to reach a predefined discrete service level, it would be desirable to derive the expected service level (in terms of available water) after a disaster.
Stephan Roolvink, Anne Remke, and Marielle Stoelinga.
"Dependability and Survivability Evaluation of a Water Distribution
Process with Arcade". Proceedings of the 9th International Workshop on
Performability Modeling of Computer and Communication Systems
PMCCS'2009 (Eger, Hungary), September 2009.
Available on-line at: http://www.vf.utwente.nl/~marielle/papers/RRS09.pdf
or from the CADP Web site in PDF or PostScript
Department of Computer Science
Formal Methods & Tools group
P.O. Box 217
7500 AE Enschede
Tel: +31 53 489 3773
Fax: +31 53 489 3247
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies