Abstract We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification’s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.

Behaviour driven formal model development (BDFMD) enables domain engineers to influence and validate mathematically precise and verified specifications. In previous work we proposed a process where manually authored scenarios are used initially to support the requirements and help the modeller. The same scenarios are used to verify behavioural properties of the model. The model is then mutated to automatically generate scenarios that have a more complete coverage than the manual ones. These automatically generated scenarios are used to animate the model in a final acceptance stage. In this paper, we discuss lessons learned from applying this BDFMD process to a real-life specification: The European Train Control Systems (ETCS) Hybrid Level 3. During the case study, we have developed our understanding of the process, modifying the way we do some stages and developing improved tool support to make the process more efficient. We discuss (1) the need for abstract scenarios during incremental model development and verification, (2) tools and techniques developed to make the running of scenarios more efficient, and (3) improvements to tools that generate new test cases to improve coverage.

Formal modelling methods rightly focus on the primary goal of verifying properties. This can however, lead to inadequate facilities for structuring the model into manageable verification components. For example, the Event-B language is designed to achieve a high level of automatic theorem proofs through a linear sequence of refinements. In previous work, we introduced a mechanism to structure models via an inclusion mechanism using event synchronisations but this did not deal with generalised instantiations of a model component. Here we introduce a lifting mechanism that can be used in conjunction with inclusion to introduce multiple instances of a separately verified model lifted to an arbitrary set of instances. This allows localised properties to be proven without the complications caused by multiple instances as well as enhancing the usability of the inclusion feature.

Event-B developments are mostly structured around the refinement relationship. This top-down development architecture enables system details to be gradually introduced into the formal model. However, this results in large models with monolithic structures. We develop a composition mechanism allowing to develop models bottom-up. In particular, our proposed mechanism works seamlessly with the existing refinement technique in Event-B. As a result we have built a formal development method that can take advantage of both top-down and bottom-up approaches. We prove the correctness of machine inclusion with refinement using the supporting Rodin platform.

Dynamic thermal management is an increasingly critical and complex part of the run-time management of many-core systems. Methods of controlling temperature include thread migration, dynamic voltage and frequency scaling and power gating using various strategies and combinations of each. In the PRiME project we are developing run-time management systems to sustain the scaling of many-core systems. As part of this development we are investigating the relative benefits of different thermal management strategies by co-simulating a Modellica model of the characteristics of a many-core device with a discrete Event-B model of the run-time manager. The results enable us to efficiently design more elaborate experiments on real hardware platforms in order to validate the run time management.

The Simulink/Stateflow (SL/SF) modeling framework is widely used in industry for the development of control applications. However, such models are not amenable to formal reasoning. Controllers can also be designed using formal specification languages. Such designs can be formally verified, but the models do not explicitly represent control or data flow information. In this paper, we discuss RRM diagrams (RRMDs), a new modelling notation which incorporates the benefits of these two formalisms. RRMDs are graphical formal models and they also support incremental formal development. We have used synchronising state machines to encode RRMDs. We have also developed a prototype tool which translates RRMDs automatically to SL/SF designs.

The emergence of the UML as a de facto standard for object-oriented modeling has been mirrored by the success of the B method as a practically useful formal modeling technique. The two notations have much to offer each other. The UML provides an accessible visualization of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilize a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specializations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioral modeling. The design of UML-B has been guided by industrial applications.