Event-B is a state-based formal method for modelling and verifying the consistency of discrete systems. Event refinement structures (ERS) augment Event-B with hierarchical diagrams, providing explicit support for workflows and refinement relationships. Despite the variety of ERS combinators, ERS still lacks the flexibility to model dynamic workflows that support dynamic changes in the degree of concurrency. Specifically in the cases where the degree of parallelism is data dependent and data values can change during execution. In this paper, we propose two types of extensions in ERS to support dynamic modelling using Event-B. The first extension is supporting data-dependent workflows where data changes are possible. The second extension improves ERS by providing exception handling support. Semantics are given to an ERS diagram by generating an Event-B model from it. We demonstrate the Event-B encodings of the proposed ERS extensions by modelling a concurrent emergency dispatch case study.

Data Integration Systems (DIS) are concerned with integrating data from multiple data sources to resolve user queries. Typically, organisations providing data sources specify security policies that impose stringent requirements on the collection, processing, and disclosure of personal and sensitive data. If the security policies were not correctly enforced by the integration component of DIS, the data is exposed to data leakage threats, e.g. unauthorised disclosure or secondary use of the data. SecureDIS is a framework that helps system designers to mitigate data leakage threats during the early phases of DIS development. SecureDIS provides designers with a set of informal guidelines written in natural language to specify and enforce security policies that capture confidentiality, privacy, and trust properties. In this paper, we apply a formal approach to model a DIS with the SecureDIS security policies and verify the correctness and consistency of the model. The model can be used as a basis to perform security policies analysis or automatically generate a Java code to enforce those policies within DIS.

Abstract Event-B is a formal method for modelling and verifying the consistency of chains of model refinements. The event refinement structure (ERS) approach augments Event-B with a graphical notation which is capable of explicit representation of control flows and refinement relationships. In previous work, the ERS approach has been evaluated manually in the development of two large case studies, a multimedia protocol and a spacecraft sub-system. The evaluation results helped us to extend the ERS constructors, to develop a systematic definition of ERS, and to develop a tool supporting ERS. We propose the ERS language which systematically defines the semantics of the ERS graphical notation including the constructors. The ERS tool supports automatic construction of the Event-B models in terms of control flows and refinement relationships. In this paper we outline the systematic definition of ERS including the presentation of constructors, the tool that supports it and evaluate the contribution that ERS and its tool make. Also we present how the systematic definition of ERS and the corresponding tool can ensure a consistent encoding of the ERS diagrams in the Event-B models.