The model that we will consider, is a very well
known one. Which is finite state machines. And you might have
seen them before. At a high level, a state machine is
a graph in which nodes represent states of the system. For
example, in this case, state 1, state 2, and state 3.
Edges represent transitions between states. For instance, in this case we
have one edge from state 1, to state 2. That means
that the system can go from state 1, to state 2.
And finally, the labels on the edges represent events
and actions. For example, what this label means is that
the system goes from state three to state two
when event five occurs. And when going from state three
to state two, it generates action four. And does
reacher model, sir reacher's kind of state machines, but we're
just going to stick to this ones which are enough. For
our purpose. So how do we build such a final
state machine starting from a specification? The first thing
we need to do is to identify the system's boundaries
and the input and output to the system. Once we
have done that, we can identify, within the boundaries of
the system, the relevant states and transitions. So we split
this single state We'll refine it into several states. And
we also identify how the system can go from one
state to another. Including which inputs cause which transition, and
which result in outputs we can obtain. To
better illustrate that, let's look at a concrete example.