Advertisement

Model Checking Correctness Properties of Electronic Contracts

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

Abstract

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.

Keywords

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

References

  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, http://www.w3.org/TR/wscl10/
  8. 8.
    Rosettanet implementation framework: core specification, V2 (January 2000), http://rosettanet.org
  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