Verifying Event-B Hybrid Models Using Cyclone

Abstract

Modelling hybrid systems using Event-B is challenging and users typically are unsure about whether their Event-B models are over/under-specified. In this short paper, we present a work-in-progress specification language called Cyclone to tackle this challenge. We demonstrate how one can use Cyclone to check an Event-B hybrid model using a car controller example. Our demonstration shows that Cyclone has a great potential to be used to verify Event-B hybrid models.

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{WuC23,
  author       = {Hao Wu and
                  Zheng Cheng},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Verifying Event-B Hybrid Models Using Cyclone},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {179--184},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_13},
  doi          = {10.1007/978-3-031-33163-3\_13},
  timestamp    = {Sun, 03 Mar 2024 18:44:21 +0100},
  biburl       = {https://dblp.org/rec/conf/zum/WuC23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}