www.prismmodelchecker.org
Home • About • Downloads • Documentation • Manual • Tutorial • Lectures • Publications • Case Studies • Support

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 and multimedia protocols

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

Other related case studies:
  • Authenticated query flooding (See [WS08])
    (Work by Frank Werner and Peter Schmitt)
  • ECo-MAC protocol for wireless sensor networks (See [ZBB10])
    (Work by Hafedh Zayani, Kamel Barkaoui and Rahma Ben Ayed)

Security

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

Other related case studies:

  • Anonymity network topologies (See [DSS04])
    (Work by Roger Dingledine, Vitaly Shmatikov and Paul Syverson)
  • Quantum cryptography protocols:
  • Various anonymity protocols: Crowds, Adithia, Onion routing and Tarzan (See [Adi06])
    (Work by M. Adithia)
  • PIN block attacks (See [Kal07])
    (Work by Eirini Kaldeli)
  • Quantification of Denial-of-Service (DoS) security threats (See [BKPA08, BKPA09])
    (Work by Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis and Nikolaos Alexiou)
  • The Kaminsky DNS cache-poisoning attack (See [ABK+10] and this page)
    (Work by Nikolaos Alexiou, Tushar Deshpande, Stylianos Basagiannis, Scott Smolka and Panagiotis Katsaros)
  • The DNS bandwidth amplification attack (See [DKBS11])
    (Work by Tushar Deshpande, Panagiotis Katsaros, Stylianos Basagiannis and Scott Smolka)
  • Non-repudiation protocols (See [LMST04, Tro06])
    (Work by Ruggero Lanotte, Andrea Maggiolo-Schettini and Angelo Troina)
  • Non-repudiation protocols (See [SM09])
    (Work by Indranil Saha and Debapriyay Mukhopadhyay)
  • A Reinforcement Model for Collaborative Security (See [MS09])
    (Work by Janardan Misra and Indranil Saha)
  • A Certified E-Mail Protocol In Mobile Environments (See [PBA+11, nBPA+11])
    (Work by S. Basagiannis, S. Petridou, N. Alexiou, G. Papadimitriou and P. Katsaros)
  • The Needham-Schroeder (NS) and TMN protocols (See [AA10])
    (Work by Mojtaba Akbarzadeh and Mohammad Abdollahi Azgomi)
  • The ASW fair exchange protocol (See [IZ08])
    (Work by Salekul Islam and Mohammad Abu Zaid)

Biology

The following examples use PRISM to study the behaviour of various biological 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 (See [CFK+12])

Performance and reliability

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

Other related case studies:
  • Cloud computing live migration (See [KM11])
    (Work by Shinji Kikuchi and Yasuhide Matsumoto at Fujitsu)
  • Publish-subscribe systems (See [HBGS07])
    (Work by Fei He, Luciano Baresi, Carlo Ghezzi and Paola Spoletini)
  • Group membership protocols (See [RSPV07])
    (Work by Valério Rosset, Pedro F. Souto, Paulo Portugal and Francisco Vasques)
  • Crossbar molecular switch memory (See [CT08])
    (Work by Ayodeji Coker and Valerie Taylor)
  • Software architectures for multi-core platforms (See [TK11])
    (Work 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 (See [SDM08])
    (Work by Aleksandra Sesic, Stanisa Dautovic and Veljko Malbasa)
  • Environmentally powered wireless sensor nodes (See [SAA+08])
    (Work 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
    (Collaboration with Michel de Rougemont)
  • The Ising model (See [STKT07, STTK09])
    (Work by Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno and Koichi Takahashi)
  • Cognitive assistive technology: The hand-washing problem (See [Ma08])
    (Work by Zhongdan Ma)

Case Studies