PEPA Nets in Practice: Modelling a Decentralised Peer-to-Peer Emergency Medical Application

Stephen Gilmore, Valentin Haenel, Jane Hillston, Leïla Kloul

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We apply the PEPA nets modelling language to modelling a peer-to-peer medical informatics application, the FieldCare PDA-based medical records system developed by SINTEF Telecom and Informatics, Norway. Medical data on accident victims is entered by medics on handheld devices at the crash site and propagated wirelessly from peer to peer in order to improve information flow and reduce the potential for data loss. The benefits of such a system include improved reliability in patient care and the ability for hospitals to prepare better for incoming trauma patients. The effectiveness and usefulness of the system in practice depends upon both reliability and performance issues. We analyse the functioning of the application through a high-level model expressed in the PEPA nets modelling language, a coloured stochastic Petri net in which the tokens are terms of Hillston’s Performance Evaluation Process Algebra (PEPA). We use the PRISM probabilistic model checker to solve the model and evaluate probabilistically quantified formulae which quantify the responsiveness of the system.
Original languageEnglish
Title of host publicationApplying Formal Methods: Testing, Performance, and M/E-Commerce
Subtitle of host publicationFORTE 2004 Workshops The FormEMC, EPEW, ITM, Toledo, Spain, October 1-2, 2004. Proceedings
EditorsManuel Núñez, Zakaria Maamar, FernandoL. Pelayo, Key Pousttchi, Fernando Rubio
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-30233-9
ISBN (Print)978-3-540-23169-1
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'PEPA Nets in Practice: Modelling a Decentralised Peer-to-Peer Emergency Medical Application'. Together they form a unique fingerprint.

Cite this