Evaluating repair strategies for a water-treatment facility using Arcade

Author

Haverkort, B.R. ; Kuntz, M. ; Remke, A. ; Roolvink, S. ; Stoelinga, M.I.A.

Author_Institution

Univ. of Twente, Enschede, Netherlands

fYear

2010

fDate

June 28 2010-July 1 2010

Firstpage

419

Lastpage

424

Abstract

The performance and dependability of critical infrastructures, such as water-treatment facilities is essential. In this paper we use various performance and dependability measures to analyze a simplified model of a water treatment facility. Building on the existing architectural framework Arcade a model is derived in XML format and then automatically mapped to the model checker PRISM. Using the stochastic model checking capabilities that PRISM offers, we compare different repair strategies, with respect to their costs, system reliability, availability and survivability. For this case study we conclude that using non-preemtive priority scheduling with additional repair crews is the best choice with respect to performance, dependability and costs.

Keywords

environmental science computing; formal verification; software architecture; stochastic processes; water treatment; Arcade; PRISM model checker; XML; critical infrastructures; nonpreemtive priority scheduling; stochastic model checking; water treatment facility; Availability; Buildings; Costs; Government; Logic design; Performance analysis; Reliability; Stochastic processes; Stochastic systems; XML;

fLanguage

English

Publisher

ieee

Conference_Titel

Dependable Systems and Networks (DSN), 2010 IEEE/IFIP International Conference on

Conference_Location

Chicago, IL

Print_ISBN

978-1-4244-7500-1

Electronic_ISBN

978-1-4244-7499-8

Type

conf

DOI

10.1109/DSN.2010.5544290

Filename

5544290