A Survey of Relevant Literature - The Unknown Component Problem: Theory and Applications - page 91

Going beyond previous ad hoc approaches, the fact of embedding logic synthesis
problems into WS1S formulas allows one to state them in a common frame, enabling
easily proof of correctness and completeness of the proposed solutions. Then the
computations are performed on the related automata applying to them the operations
that correspond to the standard logical connectives (however the result may be a
regular language that is not an FSM language, an issue addressed by Theorem 3.8).
In contrast, the theory of synchronous and parallel equations is built upon the
primitive notions of language and language composition, and models naturally a
larger spectrum of language equations and their specialized solutions.

5.1.7 Testing

When an FSM is embedded into a complex system, usually there is no direct access
to its inputs and outputs, and thus the FSM cannot be tested in isolation; the reason
is limited controllability from outside of the internal inputs of the FSM, or limited
observability from outside of the internal outputs of the FSM. This is the so-called
problem of testing in context, which has been an active area of research. Petrenko
et al. [114] proposed to solve testing in context by means of solving equations over
FSMs to derive all FSMs externally equivalent to a given component FSM, since the
latter FSMs are exactly the reductions of the largest solution describing the complete
flexibility of the given component FSM.

5.1.8 Model Matching by Simulation Relations

The objective of model matching in control theory is to design a controller M B
so that the composition of a plant M A with M B matches a given model M C
(see the controller's topology in Fig. 1.1e). A procedure for deriving the largest
solution for complete FSMs M A (DFSM) and M C (PNDFSM) of the equation M A
M X

sim M C for the discrete model matching problem was proposed in [12, 68],

sim

denotes simulation relation 3 where (as opposed to language containment in

3

S 1 S 2 is a simulation relation from an FSM M 1 Dh S 1 ;I;O;T 1 ;r 1 i to an FSM M 2 D
h S 2 ;I;O;T 2 ;r 2 i if:
1. .r 1 ;r 2 / 2 ,and
2. .s 1 ;s 2 / 2 )
f8 i 8 o 8 s 0 1 Œ.s 1

i=o
! M 2 s 0 2 / ^ .s 0 1 ;s 0 2 / 2 g .
If such a exists, we say that M 2 simulates M 1 ,orthatM 1 has a simulation into M 2 , and denote
it by M 1

i=o
! M 1 s 0 1 / )9 s 0 2 Œ.s 2

sim M 2 .