Difference between pages "D32 Scalability" and "Event-B Language"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Son
 
imported>WikiSysop
 
Line 1: Line 1:
=== Overview ===
+
== Book: Modelling in Event-B: System and Software Engineering by Jean-Raymond Abrial ==
Regarding scalability of the Rodin platform, the following contributions has been made:
+
More information about the book is at Cambridge University Press [http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569 website]
 +
=== Sample Chapters of the books ===
 +
This is available at event-b.org [http://www.event-b.org/abook.html]
 +
=== Slides and Rodin Platform archives of the developments corresponding to chapters of the books ===
 +
* Chapter 1: [http://deploy-eprints.ecs.soton.ac.uk/111/ Introduction]
 +
* Chapter 2: [http://deploy-eprints.ecs.soton.ac.uk/112/ Controlling Cars on a Bridge]
 +
* Chapter 3: [http://deploy-eprints.ecs.soton.ac.uk/113/ A Mechanical Press Controller]
 +
* Chapter 4: [http://deploy-eprints.ecs.soton.ac.uk/114/ File Transfer Protocol]
 +
* Chapter 6: [http://deploy-eprints.ecs.soton.ac.uk/115/ The Bounded Re-transmission Protocol]
 +
* Chapter 7: [http://deploy-eprints.ecs.soton.ac.uk/116/ Concurrent Program Development]
 +
* Chapter 8: [http://deploy-eprints.ecs.soton.ac.uk/117/ Electronic Circuits Development]
 +
* Chapter 10: [http://deploy-eprints.ecs.soton.ac.uk/118/ Leader Election on a Ring-shaped Network]
 +
* Chapter 11: [http://deploy-eprints.ecs.soton.ac.uk/119/ Synchronizing Processes on a Tree Network]
 +
* Chapter 12: [http://deploy-eprints.ecs.soton.ac.uk/120/ Routing Algorithm for Mobile Agent]
 +
* Chapter 13: [http://deploy-eprints.ecs.soton.ac.uk/121/ The Leader Election Protocol (IEEE1394)]
 +
* Chapter 15: [http://deploy-eprints.ecs.soton.ac.uk/122/ Sequential Program Development]
 +
* Chapter 16: [http://deploy-eprints.ecs.soton.ac.uk/123/ Location Access Controller]
 +
* Chapter 17: [http://deploy-eprints.ecs.soton.ac.uk/124/ Train System]
  
* (Alexei) Flow plug-in
+
== Event-B Language Documentation ==
  
* (Alexei) Group Refinement
+
[[Event-B Modelling Language]]
  
* (Alexei) Modes
+
[[Event-B Mathematical Language]]
  
* Emre Yilmaz and Thai Son Hoang (ETH Zurich) has developed a plug-in supporting an extension of Event-B with qualitative reasoning. The extension allows developer to declare an event converges probabilistically (with probability 1). This is in contrast with standard certain termination, where convergent events ''must decrease'' the declared variant. Provided that the variant is bounded above, an event probabilistically converges if it ''might decrease'' the variant. The extension enables Event-B to model systems with ''almost certain termination'' properties, e.g. IEEE 1394 Firewire protocol<ref name="ieee1394">J.-R. Abrial, D. Cansell, D. Mery.  A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. ''Formal Asp. of Comput.'' 14(3):215-227, 2003</ref> or Rabin's Choice Coordination algorithm <ref name="rabin">M. Rabin. The Choice Coordination Problem. ''Acta Informatica, 17:121-134'', 1982.</ref>.
+
[http://wiki.event-b.org/images/EventB-Summary.pdf Concise Summary of the Event B mathematical toolkit] by Ken Robinson
  
=== Motivations ===
+
[[Well-definedness in Event-B]]
  
==== Flow plug-in ====
+
==Modelling Tips==
(Alexei)
 
  
==== Group Refinement ====
+
[[Structured_Types]]
(Alexei)
 
  
==== Modes ====
+
[[Category:User documentation]]
(Alexei)
+
[[Category:Event-B]]
  
==== Qualitative Reasoning ====
+
== Proving Tips ==
Probability is used in many distributed systems for breaking the symmetry between different components/processes, e.g. IEEE 1394 Firewire protocol <ref name="ieee1394"/>, Rabin Choice Coordination algorithm <ref name="rabin"/>. For such systems, termination cannot be guaranteed for certain. Instead, a slightly weaker property is mostly appropriate: ''termination with probability one''. As an example for this type of systems is to consider tossing a coin until it comes up tail. Provided that the coin is fair (in that sense that no face is ignored forever), eventually, the coin will eventually come up head.
 
  
Qualitative probabilistic reasoning has been integrated into Event-B <ref name="ifm07">S. Hallerstede, T.S. Hoang. Qualitative Probabilistic Modelling in Event-B. ''iFM 2007: Integrated Formal Methods'', Oxford, U.K. July 2007</ref>: a new kind of actions is added, namely ''probabilistic actions'' with an assumption that the probability for each possible alternative is bounded away from 0 or 1.  Most of the time, probabilistic actions behave the same as (standard) non-deterministic actions (e.g. invariant preservation).  The difference between probabilistic and non-deterministic actions is with convergence proof obligation: probabilistic actions are interpreted ''angelically'', whereas non-deterministic actions are interpreted ''demonically''.  The result is a practical method for handling qualitative reasoning that generates proof obligations in the standard first-order logic of Event-B.
+
== Miscellaneous ==
 
+
* Jean-Raymond Abrial, "Faultless Systems: Yes We Can!," Computer, vol. 42, no. 9, pp. 30-36, Sept. 2009, [http://doi.ieeecomputersociety.org/10.1109/MC.2009.283 doi:10.1109/MC.2009.283].
The plug-in allows developers to declare an event to be probabilistic convergent and generate appropriate proof obligations. Since the obligations are in standard first-order logic supported by the Rodin platform, we do not need to make any extension for the provers to handle the new proof obligations.
 
 
 
=== Choices/Decisions ===
 
 
 
==== Flow plug-in ====
 
(Alexei)
 
 
 
==== Group Refinement ====
 
(Alexei)
 
 
 
==== Modes ====
 
(Alexei)
 
 
 
==== Qualitative Reasoning ====
 
* Ideally, we would like to have a new value for the '''convergence''' attribute of Event-B events.  However, this is not currently supported by the Rodin platform.  Instead, a new '''probabilistic''' attribute is defined for events, with the value is either ''standard'' or ''probabilistic''.
 
 
 
* Since standard refinement does not maintain probabilistic convergent property, we put a restriction on the development method for ''almost-certain termination systems'' as follows.
 
*# Establish the model of the systems with various ''anticipated'' events
 
*#
 
 
 
=== Available Documentation ===
 
 
 
* Master thesis of Emre Yilmaz on developing tool support for qualitative reasoning in Event-B <ref>[http://e-collection.ethbib.ethz.ch/view/eth:1677  E. Yilmaz. Tool support for qualitative reasoning in Event-B. Master's thesis, Department of Computer Science, ETH Zurich, Switzerland, Aug. 2010]</ref>.
 
 
 
* The development of Rabin's Choice Coordination Algorithm is available at the DEPLOY Repository <ref>[http://deploy-eprints.ecs.soton.ac.uk/232/ E. Yilmaz. Rabin's Choice Coordination Development.]</ref>.
 
 
 
* A paper describing the development of Rabin Choice Coordination algorithm and tool support in the Proceedings of AVoCS'10 <ref>[http://deploy-eprints.ecs.soton.ac.uk/258/ E. Yilmaz and T.S. Hoang, Development of Rabin's Choice Coordination Algorithm in Event-B. ''Proceedings of AVoCS'10'', Dusseldorf, Germany, 2010]</ref>.
 
 
 
=== Planning ===
 
 
 
==== Flow plug-in ====
 
(Alexei)
 
 
 
==== Group Refinement ====
 
(Alexei)
 
 
 
==== Modes ====
 
(Alexei)
 
 
 
==== Qualitative Reasoning ====
 
In DEPLOY's fourth year, we plan to implement the missing proof obligations. More importantly, we will investigate the interaction between refinement and almost certain termination. This allows us to prove convergence properties early in the development and make sure that refinement will maintain these convergent properties.
 
 
 
=== References ===
 
<references/>
 
 
 
[[Category:D32 Deliverable]]
 
[[Category:Books]]
 

Revision as of 16:23, 18 December 2009

Book: Modelling in Event-B: System and Software Engineering by Jean-Raymond Abrial

More information about the book is at Cambridge University Press website

Sample Chapters of the books

This is available at event-b.org [1]

Slides and Rodin Platform archives of the developments corresponding to chapters of the books

Event-B Language Documentation

Event-B Modelling Language

Event-B Mathematical Language

Concise Summary of the Event B mathematical toolkit by Ken Robinson

Well-definedness in Event-B

Modelling Tips

Structured_Types

Proving Tips

Miscellaneous

  • Jean-Raymond Abrial, "Faultless Systems: Yes We Can!," Computer, vol. 42, no. 9, pp. 30-36, Sept. 2009, doi:10.1109/MC.2009.283.