In: E-Commerce: FORTE 2004 Workshops The FormEMC, EPEW, ITM, Toledo, Spain, October 1-2, 2004: Proceedings of Applying Formal Methods: Testing, Performance, and M, pages 262-277. Volume 3236 of Lecture Notes in Computer Science / Manuel Núñez, Zakaria Maamar, Fernando L. Pelayo et al. (Eds.) --- Springer-Verlag, September 2004.
Abstract: 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.