Modeling and Model Checking Mobile Phone Payment Systems

  • Tim Kempster
  • Colin Stirling
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


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.


  1. 1.
    Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)CrossRefzbMATHGoogle Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  3. 3.
    Comer, D.E.: Internetworking with TCP/IP, vol. 1. Prentice–Hall, Upper Saddle River (1995)zbMATHGoogle Scholar
  4. 4.
    Ellson, J., Gansner, E., Koutsofios, E., North, S.: Graphviz,
  5. 5.
    Halpern, J.Y., Zuck, L.D.: A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. Journal of the ACM 39(3), 449–478 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Heintze, N., Tygar, J.D., Wing, J., Wong, H.C.: Model checking electronic commerce protocols. In: Proceedings of the Second USENIX Workshop on Electronic Commerce, pp. 147–164 (November 1996)Google Scholar
  7. 7.
    Holzmann, G.J.: The Spin model checker. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefGoogle Scholar
  8. 8.
    Day, J.D., Zimmermann, H.: The OSI reference model. Proceedings of the IEEE 71, 1334–1340 (1983)CrossRefGoogle Scholar
  9. 9.
    Kempster, T., Stirling, C., Thanisch, P.: A more committed quorumbased three phase commit protocol. In: International Symposium on Distributed Computing, pp. 246–257 (1998)Google Scholar
  10. 10.
    Lynch, N.A.: Distributed Algorithms, ch. 8. Morgan-Kaufmann, San Francisco (1993)Google Scholar
  11. 11.
    Peled, D.: Ten years of partial order reduction. LNCS, vol. 1427 (1998)Google Scholar
  12. 12.
    Stulp, F., Verbrugge, R.: A knowledge-based algorithm for the internet transmission control protocol (tcp). In: Bonanno, G., van der Hoek, W. (eds.) Proceedings 4rd Conference on Logic and the Foundations of Game and Descision Theory, LOFT 4 (2000)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Tim Kempster
    • 1
  • Colin Stirling
    • 1
  1. 1.School of InformaticsUniversity of Edinburgh, JCMBEdinburghScotland

Personalised recommendations