Modeling and Model Checking Mobile Phone Payment Systems

Tim Kempster, Colin Stirling

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


Recently a technique for transacting goods using GSM mobile phones has become very popular. We present a formal model of these novel transactions using a views based modeling technique. We show how to express two safety properties namely goods and money atomicity within this model using a sub-logic of CTL. By automatically generating a labelled transition system from our views model we can model check these properties. We show how to generalise this model to arbitrary numbers of processes. Goods atomicity fails under certain circumstances thus exposing some deficiencies that exist in existing implementations.
Original languageEnglish
Title of host publicationModeling and Model Checking Mobile Phone Payment Systems
Subtitle of host publicationFormal Techniques for Networked and Distributed Systems - FORTE 2003
EditorsHartmut König, Monika Heiner, Adam Wolisz
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-39979-7
ISBN (Print)978-3-540-20175-5
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Modeling and Model Checking Mobile Phone Payment Systems'. Together they form a unique fingerprint.

Cite this