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