Model Checking Correctness Properties of Electronic Contracts (2003)

Author(s): Solaiman E, Molina-Jimenez C, Shrivastava S

    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.

      • Book Title: Service-Oriented Computing - ICSOC 2003
      • Volume: 2910/2003
      • Pages: 303-318
      • Publisher: Springer Berlin
      • Publication type: Book chapter
      • Bibliographic status: Published

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


      Emeritus Professor Santosh Shrivastava
      Senior Research Investigator

      Dr Ellis Solaiman
      Teaching Fellow