Engineering change in a non-deterministic FSM setting

We propose a new formalism for the Engineering Change (EC) problem in a finite state machine (FSM) setting. Given an implementation that violates the specification, the problem is to alter the behavior of the implementation so that it meets the specification. The implementation can be a pseudo-nondeterministic FSM while the specification may be a nondeterministic FSM. The EC problem is cast as the existence of an “appropriate” simulation relation from the implementation into the specification. We derive the necessary and sufficient conditions for the existence of a solution to the problem. We synthesize all possible solutions, if the EC is feasible. Our algorithm works in space which is linear, and time which is quadratic, in the product of the sizes of implementation and specification. Previous formulations of the problem which admit nondeterministic specifications, although more general, lead to an algorithm which is exponential. We have implemented our procedure using Reduced Ordered Binary Decision Diagrams