Wednesday, 30 November 2011

summary: A FORMAL ANALYSIS OF A BUSINESS CONTRACT LANGUAGE

G. Governatori and Z. Milosevic. A formal analysis of a business contract language. Int. J. Cooperative Inf. Syst., 15(4):659–685, 2006.

This paper presents a formal system for describing contracts in terms of deontic concepts such as obligations, permissions and prohibitions, and the logic supports reasoning about violations of obligations in contracts. Using a formal representation for contracts. The paper first provided a sample contract to be used as an example. The showed the importance of using formal languages to represent contracts. After that stated that a formal language intended to represent contracts should provide notions related to the concepts of obligations, permissions, and entitlements.

The paper explained the FCL rules anatomy (r : ¬p,¬α |- OSupplierβ) showing that every rule should start with a unique name/id (r), then a list of conditions (¬p,¬α ), that when true, a consequence (OSupplierβ) to be applied. It also showed that FCL could represent permission, obligation, prohibition, and negation. Another useful tool used by FCL is the ‘-expression’ that can be used to repair violations. FCL can be used to analyse contracts and to reason about them so that ambiguities in a contract can be identified.

The paper then introduced a procedure that uses FCL to generate a formal (logical) form of the contract. First step to do so is to combine contract closes of obligations with the obligations that triggered in response to violations of these obligations. Second step is identifying and removing redundancies from the formal specifications, redundancy occur when the normative content of one rule (r2) are all included in another rule (r1), then we can easily say that r2 does not add anything and can be discarded. Final step is finding and solving the issue of conflicts by either creating a superiority relation over the rules () and to use it do “defeat” the weaker rule, or by supplementing the antecedent of one rule with an additional guard.

The paper then gave an explanation about BCL (Business Contract Language). BCL is to enable monitoring of contract execution in an event-based manner. The main use of event patterns in BCL is to enable checking of policies related to a contract. Policies define behavioural constraints for the roles that carry out activities in a contract and these constraints are described in terms of event patterns. Policy checking consists of identifying event patterns in activities of parties filling a role and establishing whether they satisfy the policies. The policies take a form of modal constraints such as obligations, permissions and prohibitions. A policy violation can be linked to another policy that can take effect in response to this violation.

BCL uses the following attributes:
·      Role: to label a party whose behavior is constrained by the policy. 
·      Event patterns: where events can be matched with event patterns using event type. Checking policies consists of identifying event patterns in activates. Events in BCL can have event roles, which can be linked to contract roles.
·      State: used to define data value shared by participants. It is used to maintain running totals, counters, and other states.
·      Policy: it is associated with a role and indicate wither it is an obligation, permission, or prohibition. Policy consist of a name, the role that this policy applies to, what type of modality applies, what triggers this policy, and what is the expected behavior based on this policy. It might also include a Guard that specify a specific timing when will this policy should be applied. A guard can be used to specify that a policy only will occur in case of violation of another policy.
The authors stated that even thought there are other contract languages such as Contract Expression Language, Web Services Level Agreements and ecXML. BCL “covers broader aspects, including the organisational context for the definition of policies, behaviour and structure and relationships between these concepts”.

Finally the paper introduced a mapping from FCL to BCL, and then from BCL to FCL. To map FCL to BCL, the name/id of the rule in FCL can map to the policy name in BCL. The model literal in FCL rule gives the role, modality, and expected behavior of BCL policy. Finally the condition literals in FCL rule will map to trigger in BCL policy.  The same concept can be reversed to map from BCL to FCL.

The paper then stated that BCL need a better separation between subject and target roles, also a better separation between trigger event and the action event. Another shortcoming of BCL is the lack of priorities support between rules to avoid conflicts. BCL need to be tested against the notions of delegation and authorization.



No comments:

Post a Comment