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 [ChatterjeeGK13].
  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 [DwyerAC98].
  5. Randomised Dining Philosophers: In this probabilistic version of the dining philosophers problem, we analysed a property obtained by instantiating a pattern from [DwyerAC98].
  6. Firewire: The Firewire protocol is used for high-speed data transfer. The property we analysed was derived from [DwyerAC98].