In: Proc. 19th Symp. on Reliable Distributed Systems, 16-18 October 2000, Nürnberg, Germany, pages 228-237. 2000.
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. This paper shows that the 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, the structure of CSL-specified dependability measures can be exploited 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: CSL, Markovian models, continuous stochastic logic, dependability evaluation, model checking, stochastic Petri nets.