Model Checking Failure-Prone Open Systems Using Probabilistic Automata

We consider finite-state Hierarchical Probabilistic Automata (HPA) to model failure-prone open systems. In an HPA, its states are stratified into a fixed number of levels. A k-HPA is an HPA with k + 1 levels and it can be used to model open systems where up to k failures can occur. In this paper, we present a new forward algorithm that checks universality of a 1-HPA. This algorithm runs much faster than an earlier backward algorithm. We present the implementation and experimental results for verifying abstracted failure-prone web applications. We also prove a theoretical result showing that the problem of checking emptiness and universality for 2-HPA is undecidable answering an open question.