Explicit Exploration of Refinement Design in Proof-Based Approach: Refinement Engineering in Event-B

Control of abstraction levels is key to tackling the increasing complexity of emerging systems such as cyber-physical systems. Formal methods for dependability assurance have been used to explore this point by using refinement mechanisms, with which complex models are gradually constructed and verified. However, refinement mechanisms to derive the whole specification of systems are relatively new, as with the Event-B method, and refinement design is still an “art.” In this chapter, we discuss the problem of refinement design and present our approach for explicitly exploring and manipulating possible refinement designs. Specifically, we report our experiences on refinement planning and refactoring to support engineering activities on refinement.