Proceedings of the 9th Rodin User and Developer Workshop, 2021

The Scenario Checker is a plugin tool for the Rodin platform for Event-B. It allows scenarios to be animated on Event-B models for validation purposes. Scenarios can be recorded, re-played and extended. The model can be annotated to distinguish and prioritise internal events and designate private variables. During recording , events that are designated as internal are automatically executed when enabled so that a form of ‘run to completion’ (or big step ) is provided to represent the systems responses to changes in its environment. This allows the user to focus on developing the scenario in the environment while efficiently executing the response of the system. If necessary the user can take control of the response by executing internal events singly. This may be useful when the model still contains non-deterministic behaviour. The recorded sequence of external events and the values of non-private variables at each step can be saved in a scenario file. During playback , the sequence of external events to be executed is taken from the recorded scenario file while the internal events are again fired automatically. Hence the same scenario can be replayed after the model has been changed in order to test that scenario is still correctly executed in the new version of the model. At the end of each big step, critical (i.e. non-private) variables are compared with previous recorded values in order to highlight de-viations. While replaying a scenario, the tool can be changed to record mode at any point so that an alternative ending to the scenario can be explored. This allows alternative scenarios to be efficiently developed from a common preamble. The Scenario Checker is based on the ProB model checker and can be run in parallel with state visualisation tools such as BmotionStudio (which is included within ProB) and UML-B State-machine animation. In a companion paper [1], Guillaume Verdier and Laurent Voisin presented a new approach to genericity in the Rodin toolset: this approach is made practical by means of an Instantiation Plug-in. In the present short paper 1 we propose some examples of using this new approach. Note that we constructed more examples: we only present here the most important ones. These examples are preliminary as the plug-in is still under development as stated in [1]. The key to this presentation is to show how such examples can be structured using the Instantiation Plug-in. Two basic examples are independent: Fixpoint and Wellfoundedness. Other examples depend directly or indirectly of them. This is indicated in the following diagram. The CamilleX Framework [3] provides a textual representation of Event-B models for the Rodin Platform (Rodin) platform. It supports both (1) direct extensions of the Event-B syntax to support modelling extensions such as machine inclusion [2] and record structure [1], and (2) indirect extensions via containment mechanism to such as UML-B diagrams [4]. In this presentation, we will take a look at some of the remaining issues and proposal to address them in the next release of CamilleX. Abstract Advancements in technology have improved the safety of railway transportation systems. However, railway operators face challenges when constructing and maintaining systems that use components from a variety of suppliers. Obsolescence may result in the need to replace complex components with equivalent parts while ensuring that the operation and safety of the overall system are not compromised. This abstract presents a model-based systems engineering (MBSE) approach for the specification of Deutsche Bahn's railway interlocking system (RIS) to address two issues: The first issue is the separation of the life cycles of the interlocking core and the field elements to reduce the vendor lock-in risks when upgrading or renewing railway field elements such as a level crossing, point machine etc. The second issue is achieving the required assurance that safety properties are preserved by the specification. In the EULYNX consortium, European railway infrastructure managers develop standard interfaces and subsystems for the next generation command, control and signaling (CCS) architecture. Model-based systems engineering (MBSE) is used to ensure soundness and completeness of the specified interfaces. In order to achieve this, we propose a diagrammatic MBSE framework so that safety compliant standardized models of the interface specifications can be handed over to the railway suppliers. In this framework, Infrastructure managers define the appropriate use case descriptions and modelling experts convert the use cases into executable SysML models using the Windchill Modeler3 tool. Subsequently, infrastructure managers evaluate whether the specified interfaces are sound regarding their intended use applying simulation-based testing. Modelling of the interlocking system interfaces using SysML which is a semi-formal language has already led to significant improvements in the quality of created specifications but does not allow formal verification of system properties. Our proposed framework enables the transformation of SysML models into the Event-B formal language to prove the safety requirements. Figure the overall verification and validation approach.