Changing system interfaces consistently: A new refinement strategy for CSP∥B

This paper is concerned with event refinement in the context of CSP∥B. Our motivation to include this notion within the CSP∥B 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 CSP∥B controlled components. The paper also introduces a notion of I/O refinement into our event refinement framework.

Research highlights► An approach to event refinement for CSP∥B. ► Refinement of atomic events to more detailed structures. ► Consistency between CSP and B elements of a system description and refinement. ► Interface refinement for relating abstract and concrete I/O within event refinements. ► Compositionality and consistency results for traces and traces/divergences models.