
116 Model-Based Testing for Embedded Systems
where the nodes represent states of system use and the arcs represent possible transitions
between states (see Figure 5.2). The structure together with probability distributions over
the exit arcs constitutes a Markov chain. (We note that while graphs are used in various
software engineering artifacts, they are not statistical models.)
To illustrate the theory we use a model problem, a generic patient controlled analgesia
infusion pump controller, as an example throughout the chapter. The original pump con-
troller example is given in Real-Time Systems Group, 2010. It captures the functionality
typical of ...