EB4EB, standing for Event-B for Event-B , is a framework that supports the formalisation of Event-B models using first-order logic and set-theory, so that it becomes possible to manipulate them as first-class objects. This framework relies on an Event-B algebraic theory, which serves as a meta-theory formalising, explicitly, all of the features of an Event-B machine. States, events, invariants, variants, etc... are formalised through data-types and operators. When this meta-theory is instantiated, an Event-B model becomes a first-order logic and set-theoretic formula, described in an Event-B context. Because it can handle machine elements as terms in formulas, the EB4EB framework enables the definition of new specific proof obligations and analyses . Such analyses may then be applied to any EB4EB machines in order to establish advanced properties, not natively present in the Event-B method, such as deadlock-freeness or liveness requirements. These analyses are non-intrusive since they do not require to alter the machine in order to be performed. In the previous formalisation of the EB4EB framework only states and events were handled, limiting the expressive reasoning power of the framework. This paper presents an extension of the EB4EB framework to support parameterised events, an important feature of Event-B. This extension is not straightforward in EB4EB. Indeed, the typing system supported by Event-B theories is not rich enough to describe such extension in a constructive manner as for the other Event-B features formalised in EB4EB. The proposed solution, described in this paper, consists in defining an axiomatic formalisation of event parameters definitions. We also show that the proof obligations and model analyses we have defined scale to handle event parameters. The approach is illustrated on different case studies we have developed.

For years, formal methods have been successfully applied in the railway domain to formally demonstrate safety of railway systems. Despite that, little has been done in the field of formal methods to address the cyber-physical nature of modern railway signalling systems. In this article, we present an approach for a formal development of cyber-physical railway signalling systems that is based on a refinement-based modelling and proof-based verification. Our approach utilises the Event-B formal specification language together with a hybrid system and communication modelling patterns to developing a generic hybrid railway signalling system model that can be further refined to capture a specific railway signalling system. The main technical contribution of this article is the refinement of the hybrid train Event-B model with other railway signalling sub-systems. The complete model of the cyber-physical railway signalling system was formally proved to ensure a safe rolling stock separation and prevent their derailment. Furthermore, the article demonstrates the advantage of the refinement-based development approach of cyber-physical systems, which enables a problem decomposition and in turn reduction in the verification and modelling effort.

Hybrid systems are complex systems where a software controller interacts with a physical environment, usually named a plant, through sensors and actuators. The specification and design of such systems usually rely on the description of both continuous and discrete behaviours. From complex embedded systems to autonomous vehicles, these systems became quite common, including in safety critical domains. However, their formal verification and validation as a whole is still a challenge. To address this challenge, this article contributes to the definition of a reusable and tool supported formal framework handling the design and verification of hybrid system models that integrate both discrete (the controller part) and continuous (the plant part) behaviours. This framework includes the development of a process for defining a class of basic theories and developing domain theories and then the use of these theories to develop a generic model and system-specific models. To realise this framework, we present a formal proof tool chain, based on the Event-B correct-by-construction method and its integrated development environment Rodin, to develop a set of theories, a generic model, proof processes, and the required properties for designing hybrid systems in Event-B. Our approach relies on hybrid automata as basic models for such systems. Discrete and continuous variables model system states and behaviours are given using discrete state changes and continuous evolution following a differential equation. The proposed approach is based on refinement and proof using the Event-B method and the Rodin toolset. Two case studies borrowed from the literature are used to illustrate our approach. An assessment of the proposed approach is provided for evaluating its extensibility, effectiveness, scalability, and usability.

The modern radio-based railway signalling systems aim to increase network's capacity by enabling trains to run closer to each other. At the core of such systems is train's on-board computer (discrete) responsible for computing and controlling the speed (continuous) of the train. Such systems are best captured by hybrid models, which capture discrete and continuous system's aspects. Hybrid models are notoriously difficult to model and verify, in our research we address this problem by applying hybrid systems' modelling patterns and stepwise refinement for developing hybrid train speed controller model.

Cyber-physical systems (CPS) are taking a crucial role in various areas of our society and industry. Yet, because of their hybrid nature (i.e. the integration of both continuous and discrete features), their design and verification are not easy to handle, in particular when they are part of a critical system. Their certification requires to exhibit a formal argumentation that formal methods should be able to provide. This paper addresses the formal development of CPS using correct-by-construction refinement and proof based approaches. It relies on the Event-B formal method. In addition to modeling both the discrete and continuous parts of a CPS, this paper presents a novel approach in two steps. First it shows that the generic formal model we have defined, integrating both discrete and continuous behaviors, can be instantiated by various kinds of CPS. Fundamentally, continuous behaviors modeled by differential equations mingle with discrete transition systems (mode automaton), which model discrete behaviors. Here, refinement is used as a decomposition mechanism. Second, it expands the refinement operation, well mastered in the discrete world, to cover continuous behaviors. We show that different levels of abstraction of continuous aspects can be glued in a refinement chain. The proposed approach has been completely formalized using Event-B on the Rodin platform and a case study based on water tanks is used to illustrate it.

Domain-specific modelling with domain-specific languages (DSL) is rapidly gaining popularity in both research and industry for representing models of a target domain. However for a broader adoption, MDE tools need to provide adequate support for building these DSLs as well as for using the DSLs.