Abstract.
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.
Tim Kempster: This research was supported by EPSRC grant GR/N21141.
Chapter PDF
References
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)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Comer, D.E.: Internetworking with TCP/IP, vol. 1. Prentice–Hall, Upper Saddle River (1995)
Ellson, J., Gansner, E., Koutsofios, E., North, S.: Graphviz, http://www.research.att.com/sw/tools/graphviz
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)
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)
Holzmann, G.J.: The Spin model checker. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Day, J.D., Zimmermann, H.: The OSI reference model. Proceedings of the IEEE 71, 1334–1340 (1983)
Kempster, T., Stirling, C., Thanisch, P.: A more committed quorumbased three phase commit protocol. In: International Symposium on Distributed Computing, pp. 246–257 (1998)
Lynch, N.A.: Distributed Algorithms, ch. 8. Morgan-Kaufmann, San Francisco (1993)
Peled, D.: Ten years of partial order reduction. LNCS, vol. 1427 (1998)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kempster, T., Stirling, C. (2003). Modeling and Model Checking Mobile Phone Payment Systems. In: König, H., Heiner, M., Wolisz, A. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2003. FORTE 2003. Lecture Notes in Computer Science, vol 2767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39979-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-39979-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20175-5
Online ISBN: 978-3-540-39979-7
eBook Packages: Springer Book Archive