Lookup NU author(s): Dr Carlos Molina-Jimenez,
Emeritus Professor Santosh Shrivastava
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
The paper considers a third party contract monitoring service called Contract Compliance Checker (CCC). The CCC is provided with an executable specification of the contract in force, and is capable of observing and logging the relevant business-to-business (B2B) interaction events, in order to determine whether the actions of the business partners are consistent with the contract. Naturally, it is important to ensure that the CCC itself acts correctly, which in turn implies verifying the correctness of the executable contract. To this end, a specific system design that uses event - condition - action rules for contract representation is considered and the use of a model checker for verifying correctness properties are examined. The paper shows how the CCC can be modelled as a reactive system and how its correctness requirements can be validated as safety and liveness properties. Copyright 2009 ACM.
Author(s): Molina-Jimenez C, Shrivastava S
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Proceedings of the 4th Workshop on Middleware for Service Oriented Computing, MW4SOC 2009 held at the ACM/IFIP/USENIX International Middleware Conference
Year of Conference: 2009
Publisher: ACM Press
Library holdings: Search Newcastle University Library for this item