Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems

Kristin Rutenkolk
Digital Printed Abstract View Cite
Type
Conference paper
Publication
9th International Conference on Rigorous State Based Methods (ABZ'23)

Abstract

The modeling language of classical B is used to write specifications of various systems. Tools like ProB are able to use modelchecking techniques to verify invariants of these specifications such as safety-properties. However, classical B historically supports only discrete models and has additionally no notion of floating-point numbers and real numbers. Currently challenging scenarios and issues which any suitable solution must address are explored. An approach is proposed such that ProB may offer such a solution in the future.

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{Rutenkolk23,
  author       = {Kristin Rutenkolk},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid
                  Systems},
  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        = {366--370},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_27},
  doi          = {10.1007/978-3-031-33163-3\_27},
  timestamp    = {Fri, 02 Jun 2023 21:23:53 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/Rutenkolk23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'23

Related