Dependability and Survivability Evaluation of a Water Distribution Process

Organisation:	University of Twente (THE NETHERLANDS)
Method:	Arcade Input/Output Interactive Markov Chains
Tools used:	CADP (Construction and Analysis of Distributed Processes) Arcade MRMC
Domain:	Critical Infrastructures.
Period:	2009
Size:	35,330 states and 405,112 transitions
Description:	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.
Conclusions:	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.
Publications:	[Roolvink-Remke-Stoelinga-09] 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
Contact:	Marielle Stoelinga Department of Computer Science Formal Methods & Tools group P.O. Box 217 7500 AE Enschede The Netherlands Tel: +31 53 489 3773 Fax: +31 53 489 3247 Email: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page