Abstract
Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.
This research was carried out as part of the EU research project DEPLOY (Industrial deployment of system engineering methods providing high dependability and productivity) http://www.deploy-project.eu/
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
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Event driven system construction (1999)
Abrial, J.-R.: Models of computations (1999)
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)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (to appear, 2008)
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
Abrial, J.-R., Cansell, D., Méry, D.: A mechanically proved and incremental development of IEEE 1394 tree identify protocol. Formal Aspects of Computing 14(3), 215–227 (2003)
Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition and Instantiation of Discrete Models: Application to Event-B. Fundamentae Informatica 77(1-2) (2007)
Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Back, R.-J.: Refinement Calculus II: Parallel and Reactive Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 67–93. Springer, Heidelberg (1990)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. In: Graduate Texts in Computer Science. Springer, Heidelberg (1998)
Butler, M.J.: Stepwise refinement of communicating systems. Science of Computer Programming 27(2), 139–173 (1996)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowmann, H., Derrick, J. (eds.) FMOODS 1997, vol. 2, pp. 423–438. Chapman & Hall, Boca Raton (1997)
Hallerstede, S.: Parallel hardware design in B. In: Bert, D., Bowen, J.P., King, S., Waldén, M.A. (eds.) ZB 2003. LNCS, vol. 2651, pp. 101–102. Springer, Heidelberg (2003)
Hallerstede, S., Hoang, T.S.: Qualitative probabilistic modelling in event-B. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 293–312. Springer, Heidelberg (2007)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)
Morgan, C.C.: Of wp and CSP. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, pp. 319–326. Springer, Heidelberg (1990)
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall, Englewood Cliffs (1994)
de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science 47. CUP (1998)
Roscoe, A.W.: Unbounded nondeterminism in CSP. Technical Monograph PRG-67, Programming Research Group, Oxford University (1988)
Sekerinski, E.: A calculus for predicative programming. In: Bird, R.S., Morgan, C.C., Woodcock, J.C.P. (eds.) MPC 1993. LNCS. Springer, Heidelberg (1993)
Woodcock, J., Davies, J.: Using Z. Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hallerstede, S. (2008). On the Purpose of Event-B Proof Obligations. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-87603-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87602-1
Online ISBN: 978-3-540-87603-8
eBook Packages: Computer ScienceComputer Science (R0)