Changing system interfaces consistently: A new refinement strategy for

This paper is concerned with event refinement in the context of . Our motivation to include this notion within the framework is the desire to increase flexibility in the refinement process. This approach provides the ability to change the events of CSP processes and B machines when refining a system. Notions of refinement based on traces and on traces/divergences allow abstract events to be refined by sequences of concrete events. A complementary notion of refinement between B machines is also proposed, yielding compositionality results for refinement of controlled components. The paper also introduces a notion of I/O refinement into our event refinement framework.