A High–Level Model–Checking Tool for Verifying Service Agreements

  1. Lookup NU author(s)
  2. Abukr Abdelsadiq
  3. Dr Carlos Molina-Jimenez
  4. Emeritus Professor Santosh Shrivastava
Author(s)Abdelsadiq A, Molina-Jimenez C, Shrivastava SK
Editor(s)
Publication type Conference Proceedings (inc. Abstract)
Conference NameThe 6th IEEE International Symposium on Service-Oriented System Engineering (SOSE 2011)
Conference LocationIrvine, CA
Year of Conference2011
Date12-14 December 2011
Volume
Pages297-304
ISBN9781467304115
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
In a cloud computing environment, both the client and the provider need assurances that service interactions are in accordance with the service agreement (contract). It should be possible to encode a contract as a set of executable business policies that can be evaluated by either party for controlling service interactions. Naturally, it is important to verify the cor- rectness properties of such a contract before its deployment. To this end, the paper adopts the use of model-checking techniques. A high-level model–checking tool has been developed that enables a designer to encode a contract for model checking directly as event–condition–action rules in terms of contract entities: business operations, role players with their rights, obligations and prohibitions. This not only simplifies the task of model building but also, the designer can specify the correctness requirements, in linear temporal logic, directly in terms of the contract entities. The tool has been implemented by extending the PROMELA language of the SPIN model checker.
PublisherIEEE Computer Society
URLhttp://dx.doi.org/10.1109/SOSE.2011.6139120
DOI10.1109/SOSE.2011.6139120
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item