PRISM Case Studies

PRISM has been used to analyse a wide range of case studies in many different application domains. Below you can find more information and about a large number of these. Typically, you can find descriptions of the case study and its model(s), PRISM language source code and experimental results.

We are always happy to include details of externally developed case studies. If you would like to contribute content about your work with PRISM, or you want us to add a pointer to a publication about your PRISM-related work, please contact us.

Randomised distributed algorithms

These case studies examine the correctness and performance of various randomised distributed algorithms taken from the literature.

• Randomised self-stabilising algorithms (Herman) (Israeli & Jalfon) (Beauquier et al.)
• Randomised two process wait-free test-and-set (Tromp & Vitanyi)
• Synchronous leader election protocol (Itai & Rodeh)
• Asynchronous leader election protocol (Itai & Rodeh)
• Randomised dining philosophers (Lehmann & Rabin)
• Randomised dining philosophers (Lynch, Saias & Segala)
• Dining cryptographers (Chaum)
• Randomised mutual exclusion (Rabin)
• Randomised mutual exclusion (Pnueli & Zuck)
• Randomised consensus protocol (Aspnes & Herlihy) (with Cadence SMV and PRISM) (See also [KNS01a])
• Randomised consensus protocol (Aspnes & Herlihy) (with PRISM) (See also [KNS01a])
• Byzantine agreement protocol (Cachin, Kursawe & Shoup) (with Cadence SMV and PRISM) (See also [KN02])
• Byzantine agreement protocol (Cachin, Kursawe & Shoup) (with PRISM) (See also [KN02])
• Dice programs (Knuth & Yao)

Other related case studies:

• Probabilistic leader election algorithms (Work by Wan Fokkink and Jun Pang (See [FP04])

Communication and multimedia protocols

The following case studies investigate quality of service properties of probabilistic communication and multimedia protocols.

• Bluetooth device discovery [Collaboration with Marie Duflot) (See also [DKNP04, DKNP06])
• IEEE 802.3 CSMA/CD protocol (Prototype implementation of [KNSW04])
• Bounded retransmission protocol (D'Argenio, Jeannet, Jensen & Larsen)
• IEEE 1394 FireWire root contention protocol (with PRISM) (See also [KNS03b])
• IEEE 1394 FireWire root contention protocol (with KRONOS & PRISM) (See also [DKN02, DKN04])
• IEEE 802.11 wireless LAN (See also [KNS02a])
• IPv4 Zeroconf protocol (Cheshire, Adoba & Guttman) (See also [KNPS03])
• IEEE 802.15.4 CSMA-CA protocol (ZigBee) (Work with Matthias Fruth) (See also [Fru06])
• Probabilistic broadcast protocols (Work by Ansgar Fehnker and Peng Gao) (See [FG06])
• Gossip protocol (See [KNP08d])

Other related case studies:

• Authenticated query flooding (Work by Frank Werner and Peter Schmitt) (See [WS08])

Security

These case studies use PRISM to analyse the correctness and performance of several security related systems.

• PIN cracking schemes (Contributed by Graham Steel) (See also [Ste06])
• Crowds protocol (Reiter & Rubin) (Contributed by Vitaly Shmatikov) (See also [Shm02, Shm04])
• Probabilistic contract signing (Even, Goldreich & Lempel) (Collaboration with Vitaly Shmatikov) (See also [NS06])
• Probabilistic contract signing (Ben-Or, Goldreich, Micali & Rivest) (Collaboration with Vitaly Shmatikov) (See also [NS02, NS06])
• Probabilistic fair exchange (Rabin) (Collaboration with Vitaly Shmatikov) (See also [NS06])

Other related case studies:

• Anonymity network topologies (Work by Roger Dingledine, Vitaly Shmatikov and Paul Syverson) (See [DSS04])
• Quantum cryptography protocols (Work by Rajagopal Nagarajan, Nikos Papanikolaou and Simon Gay) (See [Pap04, GNP05])
• Various anonymity protocols (Crowds, Adithia, Onion routing and Tarzan) (Work by M. Adithia) (See [Adi06])
• PIN block attacks (Work by Eirini Kaldeli) (See [Kal07])
• Quantification of Denial-of-Service (DoS) security threats (Work by S. Basagiannis, P. Katsaros, A. Pombortsis and N. Alexiou) (See [BKPA08])

Biological process modelling

The following examples use PRISM to study the behaviour of various biological processes.

• Molecular reactions (Shapiro)
• Cell cycle control in Eukaryotes (Lecca and Priami)
• FGF (Fibroblast Growth Factor) signalling (Collaboration with John Heath, Oksana Tymchyshyn) (See also [HKN+06, HKN+08])
• MAPK cascade (Huang and Ferrell) (See also [KNP08a])

Other related case studies:

• Molecular systems (Work by Roberto Barbuti, Stefano Cataudella, Andrea Maggiolo-Schettini, Paolo Milazzo and Angelo Troina) (See [BCM+04, BCM+05])
• Biological signalling pathways (Work by Muffy Calder, Vladislav Vyshemirsky, David Gilbert and Richard Orton) (See [CVGO05, CVGO06])
• Codon bias (Work by Tessa Pronk, Erik de Vink, Dragan Bosnacki and Timo Breit) (See [PVBB07])
• Ribosome kinetics (Work by Dragan Bosnacki, Tessa Pronk and Erik de Vink) (See [BPdV08])

Power management systems

These case studies investigate the performance of several power management systems.

• Dynamic power management (Collaboration with Sandeep Shukla and Rajesh Gupta) (See also [NPK+02, NPK+03])
• Real-time dynamic voltage scaling (Pillai & Shin) (See also [KNP05c])

Other related case studies:

• Dynamic power management with two-priority request queues (Work by Aleksandra Sesic, Stanisa Dautovic and Veljko Malbasa) (See [SDM08])
• Environmentally powered wireless sensor nodes (Work by Alexandru Susu, Andrea Acquaviva, David Atienza and Giovanni De Micheli) (See [SAA+08])

Reliability studies

Here, we consider reliability properties of a variety of systems.

• The thinkteam user interface (Contributed by Maurice ter Beek, Mieke Massink, Diego Latella, Stefania Gnesi, Alessandro Forghieri and Maurizio Sebastianis) (See also [BML+04, BML+05, BML05a, BML05b])
• Embedded control system (Muppala, Ciardo & Trivedi) (See also [KNP04c, KNP07b])
• NAND multiplexing (Collaboration with Sandeep Shukla) (See also [NPKS05])
• Workstation cluster (Haverkort, Hermanns & Katoen)
• Wireless communication cell (Haring, Marie, Puigjaner & Trivedi)
• Simple peer-to-peer protocol

Other related case studies:

• Publish-subscribe systems (Work by Fei He, Luciano Baresi, Carlo Ghezzi and Paola Spoletini) (See [HBGS07])
• Group membership protocols (Work by Valério Rosset, Pedro F. Souto, Paulo Portugal and Francisco Vasques) (See [RSPV07])
• Crossbar molecular switch memory (Work by Ayodeji Coker and Valerie Taylor) (See [CT08])

CTMC benchmarks

These examples are often used in the literature as benchmarks to study the efficiency of CTMC analysis techniques.

• Kanban system (Ciardo & Tilgner)
• Flexible manufacturing system (Ciardo & Trivedi)
• Cyclic server polling system (Ibe & Trivedi)
• Tandem queueing network (Hermanns, Meyer-Kayser & Siegle)

Game theory

The following case studies analyse problems related to game theory:

• Futures market investor (Collaboration with Annabelle McIver Carroll Morgan) (See also [MM05b, MM02])
• Alternating offers protocol (Rubinstein) (Contributed by Paolo Ballarini, Michael Fisher & Michael Wooldridge) (See also [BFW06])

Miscellaneous examples

• Grid world robot (Collaboration with Håkan Younes) (See also [YKNP04, YKNP06])
• Random graphs (Collaboration with Michel de Rougemont)
• The Ising model (Work by Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi) (See [STKT07])