Abstract
Hybrid Event-B includes provision for continuously varying behaviour as well as the usual discrete changes of state in the context of Event-B. As well as being able to specify hybrid behaviour in the usual way, using differential equations or continuous assignments for the continuous parts of the behaviour, looser ways of specifying behaviour at higher levels of abstraction are extremely useful. Although the need for such looser specification can be met using the logic of the formalism, certain metaphors (or patterns) occur so often, and are so useful in practice, that it is valuable to introduce special machinery into the specification language, to allow these frequently occurring patterns to be readily referred to. This paper introduces such machinery into Hybrid Event-B.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Report: Cyber-Physical Systems (2008), http://iccps2012.cse.wustl.edu/_doc/CPS_Summit_Report.pdf
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Abrial, J.-R., Su, W., Zhu, H.: Formalizing Hybrid Systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012)
Back, R.J.R., Sere, K.: Stepwise Refinement of Action Systems. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375, pp. 115–138. Springer, Heidelberg (1989)
Back, R.J.R., von Wright, J.: Trace Refinement of Action Systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)
Back, R.J., Cerschi Seceleanu, C.: Modeling and Verifying a Temperature Control System using Continuous Action Systems. In: Proc. FMICS 2000 (2000)
Back, R.J., Cerschi Seceleanu, C., Westerholm, J.: Symbolic Simulation of Hybrid Systems. In: Strooper, P., Muenchaisri, P. (eds.) Proc. APSEC 2002, pp. 147–155. IEEE Computer Society Press (2002)
Back, R.J., Petre, L., Porres, I.: Continuous Action Systems as a Model for Hybrid Systems. Nordic J. Comp. 8, 2–21 (2001)
Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core Hybrid Event-B: Adding Continuous Behaviour to Event-B (2012) (submitted)
Barolli, L., Takizawa, M., Hussain, F.: Special Issue on Emerging Trends in Cyber-Physical Systems. J. Amb. Intel. Hum. Comp. 2, 249–250 (2011)
Haggarty, R.: Fundamentals of Mathematical Analysis. Prentice Hall (1993)
Lang, S.: Real and Functional Analysis. Springer (1993)
Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer (2010)
Rodin: European Project Rodin (Rigorous Open Development for Complex Systems) IST-511599, http://rodin.cs.ncl.ac.uk/
Rudin, W.: Principles of Mathematical Analysis. McGraw-Hill (1976)
Su, W., Abrial, J.-R., Huang, R., Zhu, H.: From Requirements to Development: Methodology and Example. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 437–455. Springer, Heidelberg (2011)
Su, W., Abrial, J.-R., Zhu, H.: Complementary Methodologies for Developing Hybrid Systems with Event-B. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 230–248. Springer, Heidelberg (2012)
Sztipanovits, J.: Model integration and cyber physical systems: A semantics perspective. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, p. 1. Springer, Heidelberg (2011), http://sites.lero.ie/download.aspx?f=Sztipanovits-Keynote.pdf
Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer (2009)
Wikipedia: Absolute continuity
Willems, J.: Open Dynamical Systems: Their Aims and their Origins. Ruberti Lecture, Rome (2007), http://homes.esat.kuleuven.be/~jwillems/Lectures/2007/Rubertilecture.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Banach, R. (2013). Pliant Modalities in Hybrid Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-39698-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39697-7
Online ISBN: 978-3-642-39698-4
eBook Packages: Computer ScienceComputer Science (R0)