We propose a new formalism for the Engineering Change problem which is applicable to non-deterministic specifications. We use the notion of Simulation Relations from the theory of concurrent systems, to develop this new formalism. Our method is cast in the form of a simulation of the implementation by the specification. We prove the necessary and sufficient condition for the existence of a solution to the problem. We also provide an algorithm to obtain all possible solutions under this setting. We have implemented this algorithm, using implicit state enumeration and Reduced Ordered Binary Decision Diagrams (ROBDDs). An important feature of our method is that the algorithm gives a solution which is correct by construction, and accordingly we do not need to perform a separate verification step in the design.