DocumentCode :
1738048
Title :
On the use of model checking techniques for dependability evaluation
Author :
Haverkort, Boudewijn R. ; Hermanns, Holger ; Katoen, Joost-Pieter
Author_Institution :
Dept. of Comput. Sci., Tech. Hochschule Aachen, Germany
fYear :
2000
fDate :
2000
Firstpage :
228
Lastpage :
237
Abstract :
Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained fairly cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation
Keywords :
Markov processes; Petri nets; algebraic specification; fault tolerance; formal verification; process algebra; reliability theory; Markov chains; Markovian dependability models; continuous stochastic logic; dependability evaluation; dependability measures specification; formal syntax; model checking techniques; model specification; path-based dependability measures; semantics; state-based dependability measures; stochastic Petri nets; stochastic activity networks; stochastic process algebras; structure exploitation; Algebra; Computer science; Equations; Linear systems; Logic; Particle measurements; Petri nets; Power system modeling; Steady-state; Stochastic processes;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Reliable Distributed Systems, 2000. SRDS-2000. Proceedings The 19th IEEE Symposium on
Conference_Location :
Nurnberg
Print_ISBN :
0-7695-0543-0
Type :
conf
DOI :
10.1109/RELDI.2000.885410
Filename :
885410
Link To Document :
بازگشت