Case studies

We have successfully analysed several case studies. Most of them are taken from the PRISM webpage (our tool supports the PRISM language directly):

1. Workstation cluster: The model describes two clusters of workstations, connected by a backbone. Workstations and other components might fail with a certain rate but can be repaired afterwards. We considered properties about the order of component failures.
2. Randomised Self-Stabilising Algorithms (Israeli and Jalfon): This self-stabilising protocol is a ring-shaped network. There, several tokens might exist, the protocol tries to reduce the total number to one. We considered a property about the order of the number of tokens existing.
3. Randomised mutual exclusion: In this mutual exclusion protocol, we successfully analysed a number of properties from this paper.
4. Gossip Protocol: Gossip protocols are used to quickly spread updates to information over a network, resembling the way actual gossip works. For the version we considered, we successfully analysed a property based on a pattern formula of this paper.
5. Randomised Dining Philosophers: In this probabilistic version of the dining philosophers problem, we analysed a property obtained by instantiating a pattern from this paper.
6. Firewire: The Firewire protocol is used for high-speed data transfer. The property we analysed was derived from this paper.