Model checking correctness properties of a middleware service for contract compliance

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.