?This work was supported by Science and Engineering Research Council funded project (GR/F98055/4/1/2083).

Ming Fang, Hussein S.M. Zedan, Chris J. Ho-Stuart
Formal Systems Research Group
Department of Computer Science
University of York
Heslington, York YO1 5DD

With the increasing reliance on digital computers in embedded systems, the need to build and design and systems that deliver correct results in a timely manner has become more crucial. Large scale embedded systems are built in diverse applications such as avionics, air traffic control and patient monitoring.

Dependability may be viewed as the of a delivered service such that reliance can justifiably be placed on that service. A `correct' system is not equivalent to a totally dependable system. However, crucially, a correct system is the precondition of a dependable system. Where appropriate, reliability, fault tolerance and availability may be modelled and measured independent of verification, using probabilistic techniques and tested and improved by the use of fault tolerance mechanisms, such as recovery and diversity models.

As real-time applications become more sophisticated, the software design and development process has become increasingly more complex. The increasing complexity of software control and time-critical functions require a means for the precise specification of their behaviours and a formal method for analysing system requirements. Thus measures for both reliability and time should be represented uniformally in the formal framework.

There are several timing and probabilistic models available in the literature. However, incorporating both time and probability in a unified framework is still in its infancy. Indeed, it is not even clear what behaviour should be expected of a system when both time and probability are combined. It is therefore important to establish a set of criteria that allows judging if a particular formalism is successful in modelling such behaviours. We feel that these issues are crucial in order to have a better understanding of what we will call behaviours.

In this paper, we introduce a probabilistic model based on ideas from Markov chains. A Markov chain [BA74] is essentially a state transition model that takes a system from one state to another with a given probability. The sum of probabilities on transitions from a state is 1. Often, it is assumed that it takes one unit of time for the process to transform into the next state. Therefore Markov chains may be used to model real-time, probabilistic processes with discrete time domain. Markov chains have been used ([HJ89, RS91]) to model a large class of timed-probabilistic behaviours. Systems modelled

1

dependable trustworthy

trustworthiness

timed-probabilistic

April 27, 1992

?

1 Introduction

A Theory for Timed-Probabilistic Behaviours