Conflict analysis of deontic contracts

Abstract

Industry is currently pushing towards Service-Oriented Architectures, where code execution is not limited to the organisational borders but may be extended beyond. Typically, these sources are not accessible making it impossible to fully trust their execution. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. Composition of different services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this work we start by applying the contract language CL to the CoCoME case study in order to compare with other methods of specification. CL takes a deontic approach to specifying contracts formally. We then present a trace semantics of C.C suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into other applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk.