Difference between revisions of "Event-B Qualitative Probability User Guide"

From Event-B
Jump to: navigation, search
m (Technical References)
m (Technical References)
Line 15: Line 15:
 
* S. Hallerstede, T.S. Hoang. '''Qualitative Probabilistic Modelling in Event-B'''. In ''IFM 2007: Integrated Formal Methods, 6th International Conference Proceedings'', Oxford, UK, July 2-5, 2007, volume 4591 of LNCS © Springer-Verlag. [http://dx.doi.org/10.1007/978-3-540-73210-5_16 Springer website]
 
* S. Hallerstede, T.S. Hoang. '''Qualitative Probabilistic Modelling in Event-B'''. In ''IFM 2007: Integrated Formal Methods, 6th International Conference Proceedings'', Oxford, UK, July 2-5, 2007, volume 4591 of LNCS © Springer-Verlag. [http://dx.doi.org/10.1007/978-3-540-73210-5_16 Springer website]
 
** Initial idea about probabilistic convergence event.
 
** Initial idea about probabilistic convergence event.
 +
** New modelling elements: Variant bound
 +
** New proof obligations: '''PRV''', '''BND''', '''FINACT'''.
 +
** Example: Resolve contention in IEEE 1395 (Firewire protocol).
  
 
* E. Yilmaz, T.S. Hoang. '''Development of Rabin’s Choice Coordination Algorithm in Event-B'''.  In ''Automated Verification of Critical Systems 2010'', volume 35 of ''Electronic Communications of the EASST'' © EASST. [http://journal.ub.tu-berlin.de/eceasst/article/view/548 EASST website]
 
* E. Yilmaz, T.S. Hoang. '''Development of Rabin’s Choice Coordination Algorithm in Event-B'''.  In ''Automated Verification of Critical Systems 2010'', volume 35 of ''Electronic Communications of the EASST'' © EASST. [http://journal.ub.tu-berlin.de/eceasst/article/view/548 EASST website]
 +
** Probablistic convergence event with refinement
 +
** Constraints on how (not-) to refine probabilistic events.
 +
** Example: Rabin's Choice Coordination Algorithm.
  
 
== Usage ==
 
== Usage ==

Revision as of 12:35, 23 November 2011

User:Son at ETH Zurich is in charge of the plug-in.

Introduction

Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).


Installing and Updating

The plug-in is available through the main Rodin Update Site under Modelling Extension category.

News

  • 23.11.2011: Version 0.2.1 released for Rodin 2.3.*

Technical References

  • S. Hallerstede, T.S. Hoang. Qualitative Probabilistic Modelling in Event-B. In IFM 2007: Integrated Formal Methods, 6th International Conference Proceedings, Oxford, UK, July 2-5, 2007, volume 4591 of LNCS © Springer-Verlag. Springer website
    • Initial idea about probabilistic convergence event.
    • New modelling elements: Variant bound
    • New proof obligations: PRV, BND, FINACT.
    • Example: Resolve contention in IEEE 1395 (Firewire protocol).
  • E. Yilmaz, T.S. Hoang. Development of Rabin’s Choice Coordination Algorithm in Event-B. In Automated Verification of Critical Systems 2010, volume 35 of Electronic Communications of the EASST © EASST. EASST website
    • Probablistic convergence event with refinement
    • Constraints on how (not-) to refine probabilistic events.
    • Example: Rabin's Choice Coordination Algorithm.

Usage