Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development

Abstract

This paper presents a substitution mechanism for systems having a continuous behavior. It shall preserve the safety property stating that the output of both systems remain in a safety envelope. The whole approach is formalized using Event-B, and relies on the Rodin tools and a theory of Reals provided by the Rodin Theory Plug-in to check the internal consistency with respect to safety properties, invariants and events.

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{BabinASP16,
  author       = {Guillaume Babin and
                  Yamine A{\"{\i}}t Ameur and
                  Neeraj Kumar Singh and
                  Marc Pantel},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {Handling Continuous Functions in Hybrid Systems Reconfigurations:
                  {A} Formal Event-B Development},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {290--296},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_23},
  doi          = {10.1007/978-3-319-33600-8\_23},
  timestamp    = {Sat, 30 Sep 2023 09:34:45 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BabinASP16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}