Dependable Systems Modeling and Reliability Property Evaluation by Model Checking

Abstract:
Modeling for dependability is an established method in the domain of information systems. Most approaches dealing with structural or probabilistic modeling do not consider time information. This paper presents an approach for modeling dependable information systems for fault prediction. Established analysis techniques are applied to a particular learned model. These should reveal path to failure or time to failure. In reality, systems have a time varying behavior. The modeling technique is based on continuous time Bayesian networks (CTBN), which makes assumptions for time to transition or time to failure feasible. A drawback of CTBN is that only discrete data is processable and thus continuous variables have to be discretized. Known misbehavior (e.g. faults) is signaled by flagging auxiliary variables. The structure of the Bayesian network (BN) is learned by a Max-Min Hill-Climbing (MMHC) algorithm which also integrates the introduced auxiliary variables. A structural model generated in this way forms the backbone of a continuous time Bayesian network. CTBN parameter estimation (e.g. time characteristic) with established learning methods is hence feasible. CTBNs store parameters in a factored representation. A fusion of all these parts to an entire model is carried out with an amalgamation technique. This procedure generates a Continuous-time Markov chain (CTMC) of complete system behavior. Evaluation of CTMCs is realized with probabilistic model checking. Such an application discovers path to a failure and most likely failure states.