Abstract
Event-B has emerged as one of the dominant state-based formal techniques used for modelling control-intensive applications. Due to the blocking semantics of events, their ordering is controlled by their guards. In this paper we explore how process algebra descriptions can be defined alongside an Event-B model. We will use CSP to provide explicit control flow for an Event-B model and alternatively to provide a way of separating out requirements which are dependent on control flow information. We propose and verify new conditions on combined specifications which establish deadlock freedom. We discuss how combined specifications can be refined and the challenges arising from this. The paper uses Abrial’s Bridge example as the basis of a running example to illustrate the framework.
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.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.-R., Butler, M.J., Hallerstede, S., Voisin, L.: A Roadmap for the Rodin Toolset. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 347. Springer, Heidelberg (2008)
Butler, M.J.: csp2B: A practical approach to combining CSP and B. In: FACS, pp. 182–196 (2000)
Butler, M.J., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z. Springer, Heidelberg (2001)
Derrick, J., Wehrheim, H.: Model transformations incorporating multiple views. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 111–126. Springer, Heidelberg (2006)
Fischer, C.: CSP-OZ - a combination of CSP and Object-Z. In: Bowman, H., Derrick, J. (eds.) Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, pp. 423–438 (July 1997)
Hoang, T.S.: Personal Communication, Email (May 25, 2010)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Iliasov, A.: On Event-B and Control Flow. Technical report, School of Computing Science, Newcastle University (July 2009)
Mahony, B.P., Dong, J.S.: Blending Object-Z and timed CSP: An introduction to TCOZ. In: Futatsugi, K., Kemmerer, R., Torii, K. (eds.) 20th International Conference on Software Engineering (ICSE 1998). IEEE Press, Los Alamitos (1998)
Métayer, C., Abrial, J.-R., Voisin, L.: Event-B language. RODIN Project Deliverable 3.2, http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf (accessed 25/5/10)
Morgan, C.: Of wp and CSP. In: Beauty is Our Business: a Birthday Salute to E. W. Dijkstra, pp. 319–326 (1990)
Mussat, L.: Modéles Réactifs. Technical report, ClearSy (July 2008)
Olderog, E.-R., Wehrheim, H.: Specification and (property) inheritance in CSP-OZ. Sci. Comput. Program. 55(1-3), 227–257 (2005)
Schneider, S.: Concurrent and Real-time Systems: The CSP approach. Wiley, Chichester (1999)
Smith, G.: A semantic integration of Object-Z and CSP for the specification of concurrent systems. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 62–81. Springer, Heidelberg (1997)
Smith, G., Derrick, J.: Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP. Formal Methods in System Design 18(3), 249–284 (2001)
Treharne, H., Schneider, S.: How to drive a B machine. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 188–208. Springer, Heidelberg (2000)
Woodcock, J., Cavalcanti, A.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
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
Schneider, S., Treharne, H., Wehrheim, H. (2010). A CSP Approach to Control in Event-B. 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_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-16265-7_19
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)