Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z

ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z pp 290–296Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9675))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://wiki.event-b.org/index.php/Theory_Plug-in#Standard_Library.

References

  1. Models. http://babin.perso.enseeiht.fr/r/ABZ_2016_Models/

  2. Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)

    Book  MATH  Google Scholar 

  3. Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-B. International Journal on Software Tools for Technology Transfer 12(6), 447–466 (2010). http://dx.doi.org/10.1007/s10009-010-0145-y

    Article  Google Scholar 

  4. Babin, G., Aït-Ameur, Y., Nakajima, S., Pantel, M.: Refinement and proof based development of systems characterized by continuous functions. In: Li, X., et al. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 55–70. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25942-0_4

    Chapter  Google Scholar 

  5. Babin, G., Ait-Ameur, Y., Pantel, M.: A generic model for system substitution. In: Romanovsky, A., Ishikawa, F. (eds.) Trustworthy Cyber Physical Systems Engineering. CRC Press Taylor & Francis Group (2016)

    Google Scholar 

  6. Babin, G., Ait-Ameur, Y., Pantel, M.: Correct instantiation of a system reconfiguration pattern: a proof and refinement-based approach. In: 2016 IEEE High Assurance Systems Engineering Symposium, HASE 2016, Orlando, FL, USA, January 7–9, 2016. IEEE Computer Society Press (2016)

    Google Scholar 

  7. Banach, R.: Pliant modalities in hybrid Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 37–53. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Butler, M., Abrial, J.R., Banach, R.: From Action Systems to Distributed Systems: The Refinement Approach, chap. Modelling and Refining Hybrid Systems in Event-B and Rodin, p. 300. Taylor & Francis, February 2016. http://www.taylorandfrancis.com/books/details/9781498701587/

  9. Jastram, M.: Rodin User’s Handbook (Oct 2013). http://handbook.event-b.org

  10. Su, W., Abrial, J.R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 92(2), 164–202 (2014). http://www.sciencedirect.com/science/article/pii/S0167642314002482

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIT / INPT-ENSEEIHT, Université de Toulouse, 2 rue Charles Camichel, Toulouse, France

    Guillaume Babin, Yamine Aït-Ameur, Neeraj Kumar Singh & Marc Pantel

Authors
  1. Guillaume Babin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yamine Aït-Ameur
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Neeraj Kumar Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marc Pantel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Guillaume Babin .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Software Competence Center, Hagenberg, Austria

    Klaus-Dieter Schewe

  3. Software Competence Center, Hagenberg, Austria

    Atif Mashkoor

  4. Software Competence Center, Hagenberg, Austria

    Miklos Biro

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Babin, G., Aït-Ameur, Y., Singh, N.K., Pantel, M. (2016). Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33600-8_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33599-5

  • Online ISBN: 978-3-319-33600-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation