Maintaining semantic consistency of data is a significant problem in distributed information systems, particularly those on which a business may depend. The authors’ current work aims to use Event-B and the Rodin tools to support the specification and design of such systems in a way that integrates well into existing development processes. This paper presents ...