Toggle Main Menu Toggle Search

Open Access padlockePrints

High Level Model Checker Based Testing Of Electronic Contracts

Lookup NU author(s): Dr Ellis Solaiman, Dr Ioannis Sfyrakis, Dr Carlos Molina-Jimenez

Downloads


Licence

This is the final published version of a report that has been published in its final definitive form by School of Computing Science, University of Newcastle upon Tyne, 2016.

For re-use rights please refer to the publisher's terms and conditions.


Abstract

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 deve lWithin 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.


Publication metadata

Author(s): Solaiman E, Sfyrakis I, Molina-Jimenez C

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2016

Pages: 21

Print publication date: 01/01/2016

Acceptance date: 01/01/2016

Report Number: 1490

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://eprint.ncl.ac.uk/pub_details2.aspx?pub_id=223553


Share