Abstract
Event-B is an emerging formal method with good tool support for various kinds of system modelling. However, the control flow in Event-B consists only of non-deterministic choice of enabled events. In many applications, notably in sequential program construction, more elaborate control flow mechanisms would be convenient. This paper explores a method, based on a scheduling language, for describing the flow of control. The aim is to be able to express schedules of events; to reason about their correctness; to create and verify patterns for introducing correct control flow. The conclusion is that using patterns, it is feasible to derive efficient sequential programs from event-based specifications in many cases.
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.
References
Abrial, J.R.: Modelling in Event B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Leuschel, M., Butler, M.: ProB: An Automated Analysis Toolset for the B Method. Journal Software Tools for Technology Transfer 10(2), 185–203 (2008)
Iliasov, A.: On Event-B and control flow. Technical Report CS-TR No 1159, School of Computing Science, Newcastle University (2009)
Hallerstede, S.: Structured Event-B models and proofs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 273–286. Springer, Heidelberg (2010)
Back, R.J.R., von Wright, J.: Reasoning algebraically about loops. Acta Informatica 36, 295–334 (1999)
Abrial, J.R.: Event driven sequential program construction. Clearsy (2001), http://www.atelierb.eu/php/documents-en.php
Abrial, J.R.: Event based sequential program development: Application to constructing a pointer program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 51–74. Springer, Heidelberg (2003)
Méry, D.: Refinement-based guidelines for algorithmic systems. Int. J. Software and Informatics 3(2-3), 197–239 (2009)
Boström, P.: Creating sequential programs from Event-B models. Technical Report 955, TUCS, Turku, Finland (2009)
Hallerstede, S.: On the purpose of Event-B proof obligations. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 125–138. Springer, Heidelberg (2008)
Back, R.J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)
Back, R.J.R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium of Principles of Distributed Computing, pp. 131–142 (1983)
Back, R.J.R., Sere, K.: Stepwise refinement of action systems. Structured Programming 12, 17–30 (1991)
Butler, M.: Stepwise refinement of communicating systems. Science of Computer Programming 27, 139–173 (1996)
Butler, M.: csp2b: A practical approach to combining CSP and B. Formal Aspects of Computing 12(3), 182–198 (2000)
Plosila, J., Sere, K., Waldén, M.: Asynchronous system synthesis. Science of Computer Programming 55, 259–288 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boström, P. (2010). Creating Sequential Programs from Event-B Models. In: Méry, D., Merz, S. (eds) Integrated Formal Methods. IFM 2010. Lecture Notes in Computer Science, vol 6396. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16265-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-16265-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16264-0
Online ISBN: 978-3-642-16265-7
eBook Packages: Computer ScienceComputer Science (R0)