This paper deals with dependability of imperfect implementations
concerning given requirements. The requirements are assumed to be
written as formulas in Duration Calculus. Implementations are modeled
by continuous semi-Markov processes with finite state space, which are
expressed in the paper as finite automata with stochastic delays of
state transitions. A probabilistic model for Duration Calculus
formulas is introduced, so that the satisfaction probabilities of
Duration Calculus formulas with respect to semi-Markov processes can
be defined, reasoned about and calculated through a set of axioms and
rules of the model.