Model-Based Testing for Embedded Systems

250 Model-Based Testing for Embedded Systems

10.2.3 Describing systems by state machines

In this section, we introduce the concept of a state machine with input and output that

relates well to the introduced concept of interface. It will be used as model representing

implementations of systems.

Definition 7 (State Machine with Input and Output). Given a state space Σ, a

state machine (∆, Λ) with input and output according to the syntactic interface (I  O)

with messages over some set M consists of a set Λ ⊆Σ of initial states as well as of a state

transition function

∆:(Σ ×(I →M

∗

)) →℘(Σ ×(O →M

∗

))

By SM[I  O], we denote the set of all state machines. 

For each state σ ∈Σ and each valuation a: I → M* of the input channels in I by sequences,

we obtain