Article

The challenge of probabilistic event B

Authors:

Carroll Morgan,

Thai Son Hoang,

Jean-Raymond AbrialAuthors Info & Claims

ZB'05: Proceedings of the 4th international conference on Formal Specification and Development in Z and B

Pages 162 - 171

https://doi.org/10.1007/11415787_10

Published: 13 April 2005 Publication History

Abstract

Among the many opportunities offered by computational semantics for probability, the challenge of probabilistic Event B (pEB) is one of the most attractive.

The B method itself is now almost 20 years old, and has been much improved and adapted over that time by the many projects to which it has been applied, and by its philosophy —right from the start— that it must be practical, effective and amenable to tool support.; more recently, EventB has extended it and altered its style of use. The probabilistic-program semantics we appeal to is even older (in Kozen's original form), but has only recently been “revived” in the context of B-style abstraction and refinement.

The especial attraction of putting the two together is the likely interplay between the probabilistic theory, on the one hand, and the decades of practical experience that have by now been built-in to the B approach, on the other.

In particular, there are areas where a full theoretical treatment of probability, concurrency, abstraction and refinement —all at once— seems prohibitively complex; and yet in practice either the complexities seldom occur, or the exigencies of B's having been so-often applied to real, non-toy problems has forced it to evolve styles for avoiding such complexities. In short, we want to use (event) B to guide us towards the issues that truly are important.

Rabin's randomized mutual-exclusion algorithm is used as a motivating case study.

References

[1]

J.-R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.

Digital Library

[2]

D. Bert, J.P. Bowen, S. King, and M. Waldén, editors. Proc. 3rd Int. ZB Conference, volume 2651 of LNCS. Springer Verlag, 2003.

[3]

M.J. Butler. A CSP approach to action systems. DPhil thesis, Computing Lab., Oxford University, 1992.

[4]

M.J. Butler and C.C. Morgan. Action systems, unbounded nondeterminism and infinite traces. Formal Aspects of Computing, 7(1):37-53, 1995.

[5]

Wei Chen and J.T. Udding. Towards a calculus of data refinement. In J.L.A. van de Snepsheut, editor, Lecture Notes in Computer Science 375: Mathematics of Program Construction. Springer Verlag, June 1989.

Digital Library

[6]

E.W. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976.

Digital Library

[7]

D. Gries and J. Prins. A new notion of encapsulation. In Symposium on Language Issues in Programming Environments. SIGPLAN, June 1985.

Digital Library

[8]

Jifeng He, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In Lecture Notes in Computer Science 213, pages 187-196. Springer Verlag, 1986.

Digital Library

[9]

Jifeng He, K. Seidel, and A.K. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28:171-92, 1997. Available at {15-key HSM95}; dx.doi.org/10.1016/S0167-6423(96)00019-6.

Digital Library

[10]

Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan, and Thai Son Hoang. Development via refinement in probabilistic B -- foundation and case study. LNCS. Springer Verlag.

[11]

Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan, and Thai Son Hoang. Probabilistic invariants for probabilistic machines. In Bert et al. {2}.

[12]

D. Kozen. Semantics of probabilistic programs. Jnl. Comp. Sys. Sciences, 22:328- 50, 1981.

[13]

D. Kozen. A probabilistic PDL. Jnl. Comp. Sys. Sciences, 30(2):162-78, 1985.

[14]

Eyal Kushilevitz and M.O. Rabin. Randomized mutual exclusion algorithms revisited. In Proc. 11th Annual ACM Symp. on Principles of Distributed Computing, 1992.

Digital Library

[15]

A.K. McIver, C.C. Morgan, J.W. Sanders, and K. Seidel. Probabilistic Systems Group: Collected reports. web.comlab.ox.ac.uk/oucl/research/areas/probs.

[16]

Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Technical Monographs in Computer Science. Springer Verlag, New York, 2004.

Digital Library

[17]

Annabelle McIver, Carroll Morgan, and Thai Son Hoang. Probabilistic termination in B. In Bert et al. {2}.

Digital Library

[18]

Carroll Morgan. The generalised substitution language extended to probabilistic programs. In Didier Bert, editor, Proc. 2nd Int. B Conference, volume 1393 of LNCS. Springer Verlag, 1998. Also available at {15-B98}.

Digital Library

[19]

C.C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403-19, July 1988. Reprinted in {22}; doi.acm.org/10.1145/44501.44503.

Digital Library

[20]

C.C. Morgan. Of wp and CSP. In W.H.J. Feijen et al., editor, Beauty is Our Business. Springer Verlag, 1990.

Digital Library

[21]

C.C. Morgan, A.K. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325-53, May 1996. doi.acm.org/10.1145/229542.229547.

Digital Library

[22]

C.C. Morgan and T.N. Vickers, editors. On the Refinement Calculus. FACIT Series in Computer Science. Springer Verlag, London, 1994.

Digital Library

[23]

J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287-306, December 1987.

Digital Library

[24]

G. Nelson. A generalization of Dijkstra's calculus. ACM Transactions on Programming Languages and Systems, 11(4):517-61, October 1989.

Digital Library

[25]

M.O. Rabin. N-process mutual exclusion with bounded waiting by 4 log 2N-valued shared variable. Journal of Computer and System Sciences, 25(1):66-75, 1982.

[26]

I. Saias. Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion. In Proc. 11th Annual ACM Symp. on Principles of Distributed Computing, 1992.

Digital Library

Cited By

Aouadhi MDelahaye BLanoix A(2019)Introducing probabilistic reasoning within Event-BSoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0626-518:3(1953-1984)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s10270-017-0626-5
Amine MDelahaye BLanoix AShin SShin DLencastre M(2017)Moving from Event-B to probabilistic Event-BProceedings of the Symposium on Applied Computing10.1145/3019612.3019823(1348-1355)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019823
Brooke PPaige RPower C(2012)Approaches to modelling security scenarios with domain-specific languagesProceedings of the 20th international conference on Security Protocols10.1007/978-3-642-35694-0_6(41-54)Online publication date: 12-Apr-2012
https://dl.acm.org/doi/10.1007/978-3-642-35694-0_6
Show More Cited By

Recommendations

Moving from Event-B to probabilistic Event-B
SAC '17: Proceedings of the Symposium on Applied Computing

We propose a fully probabilistic extension of Event-B where all the non-deterministic choices are replaced with probabilities. We present the syntax and the semantics of this extension and introduce novel and adapted proof obligations for proving the ...
Undertaking the tokeneer challenge in event-b
FormaliSE '16: Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering

This paper describes a case study on the use of a formal methods tool for checking security properties of Tokeneer, a U.S. National Security Agency (NSA) project developed by Praxis, and released in 2008. We modelled Tokeneer as a series of abstract ...
Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ZB'05: Proceedings of the 4th international conference on Formal Specification and Development in Z and B

April 2005

493 pages

ISBN:3540255591

Editors:
Helen Treharne
Department of Computing, University of Surrey
,
Steve King
Department of Computer Science, University of York, Heslington, York, UK
,
Martin Henson
Department of Computer Science, University of Essex, Heslington, York, UK
,
Steve Schneider
Department of Computing, University of Surrey

Sponsors

FME
AWE: AWE
University of Surrey
BCS-FACS
Royal Holloway, University of London: Royal Holloway, University of London

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 13 April 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Aouadhi MDelahaye BLanoix A(2019)Introducing probabilistic reasoning within Event-BSoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0626-518:3(1953-1984)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s10270-017-0626-5
Amine MDelahaye BLanoix AShin SShin DLencastre M(2017)Moving from Event-B to probabilistic Event-BProceedings of the Symposium on Applied Computing10.1145/3019612.3019823(1348-1355)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019823
Brooke PPaige RPower C(2012)Approaches to modelling security scenarios with domain-specific languagesProceedings of the 20th international conference on Security Protocols10.1007/978-3-642-35694-0_6(41-54)Online publication date: 12-Apr-2012
https://dl.acm.org/doi/10.1007/978-3-642-35694-0_6
Méry DMosbah MTounsi M(2011)Refinement-based verification of local synchronization algorithmsProceedings of the 17th international conference on Formal methods10.5555/2021296.2021332(338-352)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.5555/2021296.2021332
Sun JSong SLiu Y(2010)Model checking hierarchical probabilistic systemsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939897(388-403)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939897
Hallerstede SHoang T(2007)Qualitative probabilistic modelling in event-BProceedings of the 6th international conference on Integrated formal methods10.5555/1770498.1770514(293-312)Online publication date: 2-Jul-2007
https://dl.acm.org/doi/10.5555/1770498.1770514
Abrial JButler MHallerstede SVoisin L(2006)An open extensible tool environment for event-bProceedings of the 8th international conference on Formal Methods and Software Engineering10.1007/11901433_32(588-605)Online publication date: 1-Nov-2006
https://dl.acm.org/doi/10.1007/11901433_32

View Options

View options

Figures

Tables

Media

View Table of Conten