Abstract
A case study on automotive cruise control originally done in (conventional, discrete) Event-B is reexamined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A significant case study such as this has various benefits. It can confirm that the Hybrid Event-B design allows appropriately fluent application level modelling (as is needed for serious industrial use). It also permits a critical comparison to be made between purely discrete and genuinely hybrid modelling. The latter enables application requirements to be covered in a more natural way. It also enables some inconvenient modelling metaphors to be eliminated.
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
KeYmaera, http://symbolaris.com
Report: Cyber-Physical Systems (2008), http://iccps2012.cse.wustl.edu/_doc/CPS_Summit_Report.pdf
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Antsaklis, P., Michel, A.: Linear Systems. Birkhauser (2006)
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)
Butler, M.: Towards a Cookbook for Modelling and Refinement of Control Problems (2009), http://deploy-eprints.ecs.soton.ac.uk/108/1/cookbook.pdf
Carloni, L., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.: Languages and Tools for Hybrid Systems Design. Foundations and Trends in Electronic Design Automation 1, 1–193 (2006)
DEPLOY: European Project DEPLOY IST-511599, http://www.deploy-project.eu/
Dorf, R., Bishop, R.: Modern Control Systems. Pearson (2010)
Dutton, K., Thompson, S., Barraclough, B.: The Art of Control Engineering. Addison-Wesley (1997)
Loesch, F., Gmehlich, R., Grau, K., Mazzara, M., Jones, C.: Project DEPLOY, Deliverable D19: Pilot Deployment in the Automotive Sector (2010), http://www.deploy-project.eu/pdf/D19-pilot-deployment-in-the-automotive-sector.pdf
MATLAB and SIMULINK, http://www.mathworks.com
Mermet, J.: UML-B: Specification for Proven Embedded Systems Design. Springer (2004)
Ogata, K.: Modern Control Engineering. Pearson (2008)
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/
Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. TOSEM 15, 92–122 (2006)
Snook, C., Oliver, I., Butler, M.: The UML-B Profile for Formal Systems Modelling in UML. UML-B Specification for Proven Embedded Systems Design (2004)
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)
White, J., Clarke, S., Groba, C., Dougherty, B., Thompson, C., Schmidt, D.: R&D Challenges and Solutions for Mobile Cyber-Physical Applications and Supporting Internet Services. J. Internet Serv. Appl. 1, 45–56 (2010)
Willems, J.: Open Dynamical Systems: Their Aims and their Origins. Ruberti Lecture, Rome (2007), http://homes.esat.kuleuven.be/jwillems/Lectures/2007/Rubertilecture.pdf
Yeganefard, S., Butler, M.: Control Systems: Phenomena and Structuring Functional Requirement Documents. In: Proc. ICECCS-2012, pp. 39–48. IEEE (2012)
Yeganefard, S., Butler, M., Rezazadeh, A.: Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B. In: Proc. 2nd NFM, NASA/CP-2010-216215, pp. 182–191. NASA (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banach, R., Butler, M. (2013). Cruise Control in Hybrid Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)