D32 Scalability: Difference between revisions
imported>Son |
imported>Son |
||
| Line 23: | Line 23: | ||
==== Qualitative Reasoning ==== | ==== Qualitative Reasoning ==== | ||
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. | 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''. | |||
=== Choices/Decisions === | === Choices/Decisions === | ||
Revision as of 12:29, 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. 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[1] or Rabin's Choice Coordination algorithm [2].
Motivations
Flow plug-in
(Alexei)
Group Refinement
(Alexei)
Modes
(Alexei)
Qualitative Reasoning
Probability is used in many distributed systems for breaking the symmetry between different components/processes, e.g. IEEE 1394 Firewire protocol [1], Rabin Choice Coordination algorithm [2]. 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 [3]: 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.
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 [4].
- The development of Rabin's Choice Coordination Algorithm is available at the DEPLOY Repository [5].
- A paper describing the development of Rabin Choice Coordination algorithm and tool support in the Proceedings of AVoCS'10 [6].
Planning
Flow plug-in
(Alexei)
Group Refinement
(Alexei)
Modes
(Alexei)
Qualitative Reasoning
References
- ↑ 1.0 1.1 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
- ↑ 2.0 2.1 M. Rabin. The Choice Coordination Problem. Acta Informatica, 17:121-134, 1982.
- ↑ S. Hallerstede, T.S. Hoang. Qualitative Probabilistic Modelling in Event-B. iFM 2007: Integrated Formal Methods, Oxford, U.K. July 2007
- ↑ E. Yilmaz. Tool support for qualitative reasoning in Event-B. Master's thesis, Department of Computer Science, ETH Zurich, Switzerland, Aug. 2010
- ↑ E. Yilmaz. Rabin's Choice Coordination Development.
- ↑ E. Yilmaz and T.S. Hoang, Development of Rabin's Choice Coordination Algorithm in Event-B. Proceedings of AVoCS'10, Dusseldorf, Germany, 2010
