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.
Chapter PDF
Similar content being viewed by others
Keywords
References
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)
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)
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)
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)
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)
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)
Web Service Conversation Language (WSCL) 1.0, http://www.w3.org/TR/wscl10/
Rosettanet implementation framework: core specification, V2 (January 2000), http://rosettanet.org
Holzmann, G.J.: The Model Checker Spin. IEEE Transactions on Software Engineering 23(5) (May 1997)
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)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4) (October 1985)
Solaiman, E.: University of Newcastle upon Tyne, PhD Theses (in preparation)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Solaiman, E., Molina-Jimenez, C., Shrivastav, S. (2003). Model Checking Correctness Properties of Electronic Contracts. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.P., Yang, J. (eds) Service-Oriented Computing - ICSOC 2003. ICSOC 2003. Lecture Notes in Computer Science, vol 2910. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24593-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-24593-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20681-1
Online ISBN: 978-3-540-24593-3
eBook Packages: Springer Book Archive