Multi-model Animation with JeB

A challenge posed by model-based formal methods such as Event-B is the validation of the models. This has been recognized and some tools have been created to provide modelers with means to animate models and to explore their behaviour through graphical display. These tools are quite effective on standalone models but lack the ability to connect the model to other external models. CPS systems fall under this category, as well as systems built of components interacting through a communication network. In the context of Jeb, an animation tool for Event-B models based on JavaScript, we explore the possibility of connecting models through Websockets. The paper presents a simple protocol to connect simulations. Using an example inspired by the Lung Ventilator case study, it shows how the implementation expands JeB functionality without modifying its core.