Model Checking Correctness Properties of Electronic Contracts

  • Ellis Solaiman
  • Carlos Molina-Jimenez
  • Santosh Shrivastav
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2910)


Converting a conventional contract into an electronic equivalent is not trivial. The difficulties are caused by the ambiguities that the original human-oriented text is likely to contain. In order to detect and remove these ambiguities the contract needs to be described in a mathematically precise notation before the description can be subjected to rigorous analysis. This paper identifies and discusses a list of correctness requirements that a typical executable business contract should satisfy. Next the paper shows how relevant parts of standard conventional contracts can be described by means of Finite State Machines (FSMs). Such a description can then be subjected to model checking. The paper demonstrates this using Promela language and the Spin validator.


Contract electronic contract finite state machine contract representation contract enforcement model-checking validation correctness requirements safety and liveness properties 


  1. 1.
    Goodchild, A., Herring, C., Milosevic, Z.: Business Contract for B2B. In: Proceedings of the CAISE 2000 Workshop on Infrastructure for Dynamic Business-to- Business Service Outsourcing, Stockholm, June 5-6 (2000)Google Scholar
  2. 2.
    Milosevic, Z., Dromey, R.G.: On Expressing and Monitoring Behaviour in Contracts. In: Proceedings of the 6th International Enterprise Distributed Object Computing Conference (EDOC2000), Lausanne, Switzerland, September 17-20 (2002)Google Scholar
  3. 3.
    Marjanovic, O., Milosevic, Z.: Towards Formal Modeling of e-Contracts. In: Proceedings of the 5th International Enterprise Distributed Object Computing Conference (EDOC 2001), Seattle, WA, USA, September 4-7, IEEE Computer Society, Los Alamitos (2001)Google Scholar
  4. 4.
    Abrahams, A.S., Eyers, D.M., Bacon, J.M.: Mechanical Consistency Analysis for Business Contracts and Policies. In: Proc 5th International Conference on Electronic Commerce Research (ICECR5), Montreal, Canada, October 23-27 (2002)Google Scholar
  5. 5.
    Lupu, E., Sloman, M., Dulay, N., Damianou, N.: Ponder: Realising Enterprise Viewpoint Concepts. In: Proceedings of the 4th International Enterprise Distributed Object Computing Conference (EDOC2000), Makuhari, Japan, September 25-28 (2000)Google Scholar
  6. 6.
    Molina-Jimenez, C., Shrivastava, S., Solaiman, E., Warne, J.: Contract Representation for Run-time Monitoring and Enforcement. In: Proc. IEEE Int. Conf. on ECommerce (CEC-2003), Newport Beach, California (June 2003)Google Scholar
  7. 7.
    Web Service Conversation Language (WSCL) 1.0,
  8. 8.
    Rosettanet implementation framework: core specification, V2 (January 2000),
  9. 9.
    Holzmann, G.J.: The Model Checker Spin. IEEE Transactions on Software Engineering 23(5) (May 1997)Google Scholar
  10. 10.
    Naumovich, G., Clarke, L.A.: Classifying Properties: An Alternative to the Safety- Liveness Classification. In: Proceedings of the Eighth International Symposium on the Fundations of Software Engineering (November 2000)Google Scholar
  11. 11.
    Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4) (October 1985)Google Scholar
  12. 12.
    Solaiman, E.: University of Newcastle upon Tyne, PhD Theses (in preparation)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Ellis Solaiman
    • 1
  • Carlos Molina-Jimenez
    • 1
  • Santosh Shrivastav
    • 1
  1. 1.School of Computing ScienceUniversity of Newcastle upon TyneNewcastle upon TyneEngland

Personalised recommendations