Article

Qualitative probabilistic modelling in event-B

Authors:

Stefan Hallerstede,

Thai Son HoangAuthors Info & Claims

IFM'07: Proceedings of the 6th international conference on Integrated formal methods

Pages 293 - 312

Published: 02 July 2007 Publication History

Abstract

Event-B is a notation and method for discrete systems modelling by refinement. We introduce a small but very useful construction: qualitative probabilistic choice. It extends the expressiveness of Event-B allowing us to prove properties of systems that could not be formalised in Event-B before. We demonstrate this by means of a small example, part of a larger Event-B development that could not be fully proved before. An important feature of the introduced construction is that it does not complicate the existing Event-B notation or method, and can be explained without referring to the underlying more complicated probabilistic theory. The necessary theory [18] itself is briefly outlined in this article to justify the soundness of the proof obligations given. We also give a short account of alternative constructions that we explored, and rejected.

References

[1]

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

Digital Library

[2]

Abrial, J.-R.: Event driven system construction (1999).

[3]

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).

[4]

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).

Digital Library

[5]

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).

[6]

Abrial, J.-R., Cansell, D., Méry, D.: Refinement and Reachability in Event B. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 222-241. Springer, Heidelberg (2005).

Digital Library

[7]

Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition and Instantiation of Discrete Models: Application to Event-B. Fundamentae Informatica, vol. 77(1-2) (2007).

Digital Library

[8]

Back, R.-J.: Refinement Calculus II: Parallel and Reactive Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Stepwise Refinement of Distributed Systems. LNCS, vol. 430, pp. 67-93. Springer, Heidelberg (1990).

Digital Library

[9]

Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998).

Digital Library

[10]

Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ (1976).

Digital Library

[11]

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).

Digital Library

[12]

Hallerstede, S.: Justifications for the Event-B Modelling Notation. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 49-63. Springer, Heidelberg (2006).

Digital Library

[13]

Hallerstede, S., Butler, M.J.: Performance analysis of probabilistic action systems. Formal Aspects of Computing 16(4), 313-331 (2004).

[14]

Hoang, T.S.: The Development of a Probabilistic B-Method and a Supporting Toolkit. PhD thesis, School of Computer Science and Engineering -- The University of New South Wales (July 2005).

[15]

Hoang, T.S., Jin, Z., Robinson, K., McIver, A., Morgan, C.: Probabilistic Invariants for Probabilistic Machines. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 240-259. Springer, Heidelberg (2003).

Digital Library

[16]

IEEE. IEEE Standard for a High Performance Serial Bus. Std 1394-1995 (1995).

[17]

EEE. IEEE Standard for a High Performance Serial Bus (supplement). Std 1394a- 2000 (2000).

[18]

McIver, A., Morgan, C., Hoang, T.S.: Probabilistic termination in B. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 216-239. Springer, Heidelberg (2003).

Digital Library

[19]

Morgan, C.: The Generalised Substitution Language Extended to Probabilistic Programs. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, Springer, Heidelberg (1998) Also available at {22, B98}.

Digital Library

[20]

Morgan, C., Hoang, T.S., Abrial, J.-R.: The challenge of probabilistic event B - extended abstract. In: Treharne, H., King, S., Henson, M.C., Schneider, S.A. (eds.) ZB 2005. LNCS, vol. 3455, pp. 162-171. Springer, Heidelberg (2005).

Digital Library

[21]

Morgan, C., McIver, A.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005).

Digital Library

[22]

PSG. Probabilistic Systems Group: Collected Reports. At, http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html

[23]

Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley-Interscience, New York (1994).

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: 18-Jul-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
Mashkoor AHasan O(2012)Formal probabilistic analysis of cyber-physical transportation systemsProceedings of the 12th international conference on Computational Science and Its Applications - Volume Part III10.1007/978-3-642-31137-6_32(419-434)Online publication date: 18-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31137-6_32
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 ...
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 ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

IFM'07: Proceedings of the 6th international conference on Integrated formal methods

July 2007

660 pages

ISBN:9783540732099

Editors:
Jim Davies
Oxford University Computing Laboratory, Oxford, UK
,
Jeremy Gibbons
Oxford University Computing Laboratory, Oxford, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 02 July 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
1
Total Downloads

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

Reflects downloads up to 22 Nov 2024

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: 18-Jul-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
Mashkoor AHasan O(2012)Formal probabilistic analysis of cyber-physical transportation systemsProceedings of the 12th international conference on Computational Science and Its Applications - Volume Part III10.1007/978-3-642-31137-6_32(419-434)Online publication date: 18-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31137-6_32
Hoang TAbrial J(2011)Reasoning about liveness properties in event-BProceedings of the 13th international conference on Formal methods and software engineering10.5555/2075089.2075128(456-471)Online publication date: 26-Oct-2011
https://dl.acm.org/doi/10.5555/2075089.2075128
Tarasyuk ATroubitsyna ELaibinis L(2011)Quantitative verification of system safety in event-BProceedings of the Third international conference on Software engineering for resilient systems10.5555/2045537.2045542(24-39)Online publication date: 29-Sep-2011
https://dl.acm.org/doi/10.5555/2045537.2045542
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
Blech J(2011)Probabilistic compositional reasoning for guaranteeing fault tolerance propertiesProceedings of the 15th international conference on Principles of Distributed Systems10.1007/978-3-642-25873-2_16(222-234)Online publication date: 13-Dec-2011
https://dl.acm.org/doi/10.1007/978-3-642-25873-2_16
Tarasyuk ATroubitsyna ELaibinis L(2010)Towards probabilistic modelling in event-BProceedings of the 8th international conference on Integrated formal methods10.5555/1929463.1929483(275-289)Online publication date: 11-Oct-2010
https://dl.acm.org/doi/10.5555/1929463.1929483
Tarasyuk ATroubitsyna ELaibinis LSerugendo GFitzgerald J(2010)Augmenting formal development of control systems with quantitative reliability assessmentProceedings of the 2nd International Workshop on Software Engineering for Resilient Systems10.1145/2401736.2401743(61-70)Online publication date: 15-Apr-2010
https://dl.acm.org/doi/10.1145/2401736.2401743
Hasan OTahar S(2010)Formal probabilistic analysisProceedings of the Second international conference on Abstract State Machines, Alloy, B and Z10.1007/978-3-642-11811-1_2(2-19)Online publication date: 22-Feb-2010
https://dl.acm.org/doi/10.1007/978-3-642-11811-1_2
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents