Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B

Issue title: This is a SPECIAL ISSUE ON ASM'05

Article type: Research Article

Authors: Abrial, Jean-Raymond | Hallerstede, Stefan

Affiliations: ETH Zurich, Switzerland. E-mail: {jabrial,halstefa}@inf.ethz.ch

Abstract: We argue that formal modeling should be the starting point for any serious development of computer systems. This claim poses a challenge for modeling: at first it must cope with the constraints and scale of serious developments. Only then it is a suitable starting point. We present three techniques, refinement, decomposition, and instantiation, that we consider indispensable for modeling large and complex systems. The vehicle of our presentation is Event-B, but the techniques themselves do not depend on it.

Keywords: Refinement, Decomposition, Generic Instantiation, Event-B

Journal: Fundamenta Informaticae, vol. 77, no. 1-2, pp. 1-28, 2007