Difference between revisions of "D32 Scalability"

From Event-B
Jump to: navigation, search
m (Overview)
m (Overview)
Line 8: Line 8:
 
* (Alexei) Modes
 
* (Alexei) Modes
  
* Emre Yilmaz and Thai Son Hoang (ETH Zurich) has developed a plug-in for 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. Providing that the variant is bounded above, an event probabilistically converges if it ''might decrease'' the variant.
+
* Emre Yilmaz and Thai Son Hoang (ETH Zurich) has developed a plug-in for 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. Providing 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 or Rabin's Choice Coordination algorithm.
  
 
=== Motivations ===
 
=== Motivations ===

Revision as of 12:26, 1 December 2010

Overview

Regarding scalability of the Rodin platform, the following contributions has been made:

  • (Alexei) Flow plug-in
  • (Alexei) Group Refinement
  • (Alexei) Modes
  • Emre Yilmaz and Thai Son Hoang (ETH Zurich) has developed a plug-in for 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. Providing 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 or Rabin's Choice Coordination algorithm.

Motivations

Flow plug-in

(Alexei)

Group Refinement

(Alexei)

Modes

(Alexei)

Qualitative Reasoning

Choices/Decisions

Flow plug-in

(Alexei)

Group Refinement

(Alexei)

Modes

(Alexei)

Qualitative Reasoning

Available Documentation

  • Master thesis of Emre Yilmaz on developing tool support for qualitative reasoning in Event-B [1].
  • The development of Rabin's Choice Coordination Algorithm is available at the DEPLOY Repository [2].
  • A paper describing the development of Rabin Choice Coordination algorithm and tool support in the Proceedings of AVoCS'10 [3].

Planning

Flow plug-in

(Alexei)

Group Refinement

(Alexei)

Modes

(Alexei)

Qualitative Reasoning

References