www.prismmodelchecker.org

PRISM Case Studies

PRISM has been used to analyse a wide range of case studies in many different application domains. A non-exhaustive list of these is given below. In many cases, we provide detailed information about the case study, including PRISM language source code and experimental results. For others, we just include links to the relevant publication.

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.

If you are interested in PRISM models for the purposes of benchmarking, see also the PRISM benchmark suite.

Randomised distributed algorithms

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

Other related case studies:

Communication, network and multimedia protocols

The following case studies investigate properties such as quality of service for (probabilistic) communication, network and multimedia protocols.

Other related case studies:
  • Authenticated query flooding [WS08] (by Frank Werner and Peter Schmitt)
  • ECo-MAC protocol for wireless sensor networks [ZBB10]
    (by Hafedh Zayani, Kamel Barkaoui and Rahma Ben Ayed)
  • Congestion control in vehicular ad-hoc networks (VANETs) [KF11] (by Savas Konur and Michael Fisher)

Security

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

Contract signing and fair exchange protocols:

Anonymity:

Threats and attacks:

  • PIN cracking schemes [Ste06] (see also this WIRED article) (contributed by Graham Steel)
  • PIN block attacks [Kal07] (by Eirini Kaldeli)
  • Quantification of Denial-of-Service (DoS) security threats [BKPA08, BKPA09]
    (by Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis and Nikolaos Alexiou)
  • The Kaminsky DNS cache-poisoning attack [ABK+10] (see also this page)
    (by Nikolaos Alexiou, Tushar Deshpande, Stylianos Basagiannis, Scott Smolka and Panagiotis Katsaros)
  • The DNS bandwidth amplification attack [DKBS11]
    (by Tushar Deshpande, Panagiotis Katsaros, Stylianos Basagiannis and Scott Smolka)

Quantum cryptography protocols:

Other security studies:

  • Non-repudiation protocol (Markowitch & Roggeman) [NPS13]
  • Network Virus Infection [KNPV09]
  • Non-repudiation protocols
    [LMST04, Tro06] (by Ruggero Lanotte, Andrea Maggiolo-Schettini and Angelo Troina)
    [SM09] (by Indranil Saha and Debapriyay Mukhopadhyay)
  • A Reinforcement Model for Collaborative Security [MS09]
    (by Janardan Misra and Indranil Saha)
  • A Certified E-Mail Protocol In Mobile Environments [PBA+11, BPA+11]
    (by Stylianos Basagiannis, Sophia Petridou, Nikolaos Alexiou, Georgios Papadimitriou and Panagiotis Katsaros)
  • The Needham-Schroeder (NS) and TMN protocols [AA10]
    (by Mojtaba Akbarzadeh and Mohammad Abdollahi Azgomi)
  • SSL Handshake Protocol in Mobile Communications [PB12]
    (by Sophia Petridou and Stylianos Basagiannis)

Biology

The following examples use PRISM to study the behaviour of various biological or biology-inspired processes.

The PRISM tutorial also includes a PRISM model of:

Other related case studies:

Planning and synthesis

These case studies use PRISM to synthesise and/or analyse strategies and controllers:

Game theory

The following case studies relate to or use game-theoretic concepts and techniques:

Other related case studies:
  • Collective decision making for sensor networks [CFK+12, CFK+13b]
  • Trust models for user-centric networks [KPS13]

Performance and reliability

These case studies consider performance and reliability properties of a variety of systems.

Other related case studies:
  • Cloud computing live migration [KM11]
    (by Shinji Kikuchi and Yasuhide Matsumoto at Fujitsu)
  • Publish-subscribe systems [HBGS07]
    (by Fei He, Luciano Baresi, Carlo Ghezzi and Paola Spoletini)
  • Group membership protocols [RSPV07]
    (by Valério Rosset, Pedro F. Souto, Paulo Portugal and Francisco Vasques)
  • Crossbar molecular switch memory [CT08]
    (by Ayodeji Coker and Valerie Taylor)
  • Software architectures for multi-core platforms [TK11]
    (by Li Tan and Axel Krings)

Power management

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

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

CTMC benchmarks

These examples are often used in the literature as benchmarks to study the efficiency of CTMC analysis techniques. You can find a wider selection of benchmarks, for all models, in the PRISM benchmark suite.

Miscellaneous

  • Random graphs
    (with Michel de Rougemont)
  • The Ising model [STKT07, STTK09]
    (by Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno and Koichi Takahashi)
  • Cognitive assistive technology: The hand-washing problem [Ma08]
    (by Zhongdan Ma)

Case Studies