High Level Model Checker Based Testing of Electronic Contracts.

Ellis Solaiman, Ioannis Sfyrakis, Carlos Molina-Jiménez

Research output: Contribution to journalConference articlepeer-review


Within cloud and Internet-based collaborative settings, a business contract (service agreement) is a specification that describes permissible interactions between partners. Specifically, a business contract stipulates what operations the business partners have the rights, obligations or prohibitions to execute; it also specifies when the operations are to be executed and in which order. The main purpose of an electronic contract is to regulate (monitor and/or enforce) electronic service exchanges between the contracted parties, making sure that participants adhere to the service agreement in place. Because of the dynamic nature of Internet and cloud-based relationships, the rapidity at which electronic contracts are constructed, verified for correctness, tested, and deployed is an extremely important factor. This paper describes a model checker based framework for supporting automated testing and deployment of electronic contracts. The central components of the framework are a contract monitoring service called the Contract Compliance Checker (CCC), the SPIN model checker coupled with EPROMELA, a high-level language developed specifically for modeling electronic contracts, and the LTL Manager; a graphical tool developed in order to aid with the specification of correctness properties in Linear Temporal Logic (LTL). We describe how the LTL Manager can used to create a repository of common contract related LTL templates, which then can be easily selected and parameterized by the contract designer. We also describe how SPIN can be used to automatically generate execution sequences from an EPROMELA model of a contract, and how such sequences can then be used to test the correctness of the model equivalent electronic contract deployed to the CCC.
Original languageEnglish
Pages (from-to)193-215
JournalCommunications in Computer and Information Science
Publication statusPublished - 3 Feb 2016
Event5th International Conference on Cloud Computing and Services Science - Lisbon, Portugal
Duration: 20 May 201522 May 2015

Bibliographical note

DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.


Dive into the research topics of 'High Level Model Checker Based Testing of Electronic Contracts.'. Together they form a unique fingerprint.

Cite this