ABSTRACT
Abstract. The design by contract approach enables rigorous development of componentbased software systems. In particular, it allows us to ensure component interoperability. However, defining the contracts themselves is often a challenging task, especially in the development of decentralised systems with complex component interdependencies. In this paper, we propose a refinement-based approach facilitating definition of contracts and ensuring component interoperability. The approach is based on the Event-B formalism and its modularisation extension. In the Event-B refinement process, we gradually introduce a representation of inter-component communication, distribute the global state space between the components, and decouple them. Finally, we decompose the resulting system specification into independent modules by formally defining module interfaces, obtaining at the same time component contracts. This allows us to propagate the system level properties into the component contracts and ensure component interoperability. The proposed approach is illustrated by an example – an auction system.
