Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B

This paper introduces action refinement in the context of CSP B. Our motivation to include this notion of refinement within the CSP B framework is the desire to increase flexibility in the refinement process. We introduce the ability to change the events of a CSP process and the B machines when refining a system. Notions of refinement based s and on traces/divergences are introduced in which abstract events are refined by sequences of concrete events. A complementary notion of refinement between B machines is also introduced, yielding compositionality results for refinement of CSP B controlled components. The paper also introduces a notion of I/O refinement into our action refinement framework.

• Type: Journal
• Year: 2009
• Where: IFM
• Authors: Steve Schneider, Helen Treharne
• Keywords: Action Refinement, Action Refinement Framework, Formal Methods, IFM 2009, Refinement Process