Multi-model Animation with JeB

Abstract

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Jacquot24,
  author       = {Jean{-}Pierre Jacquot},
  editor       = {Silvia Bonfanti and
                  Angelo Gargantini and
                  Michael Leuschel and
                  Elvinia Riccobene and
                  Patrizia Scandurra},
  title        = {Multi-model Animation with JeB},
  booktitle    = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
                  2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14759},
  pages        = {223--232},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63790-2\_16},
  doi          = {10.1007/978-3-031-63790-2\_16},
  timestamp    = {Thu, 04 Jul 2024 22:05:23 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/Jacquot24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}