Behavior-preserving transformations for design-for-test

An important aspect in the design of hardware/software systems is design-for-test. Improving the testability of a hardware/software system typically implies improving the controllability and observability of the internal system behavior. This can be achieved by introducing Points of Control and Observation (PCOs) in a system. We examine the effects of PCO insertion in a behavioral system specification expressed in the CCS process algebra. We define a collection of behavior-preserving transformations that enable PCOs to be inserted in a correct way, i.e. without disturbing the initial system behavior. The transformations are proven to preserve the observational system behavior and therefore they make the time-consuming process of a posteriori formal verification superfluous.