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.
CITATION STYLE
Solaiman, E., Molina-Jimenez, C., & Shrivastava, S. (2003). Model checking correctness properties of electronic contracts. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2910, 303–318. https://doi.org/10.1007/978-3-540-24593-3_21
Mendeley helps you to discover research relevant for your work.