Generating Correct Protocols from Contracts: A Commitment-Based Approach

Business contracts are used to govern inter-service interactions. These contracts are often designed by hand and typically adopted by the contract participants after manual analysis. Usually, these contracts are quite complex and involved. Additionally, manual analysis cannot guarantee to the participants whether they would financially benefit from (or at least, not suffer from) participating in the contract. As an initial attempt towards addressing this issue, our earlier work formally defined two notions of contract correctness, wherein a contract is beneficial (resp. safe) for a participant if participating in the contract would leave the participant better off (resp. not worse off) than before. In this paper, we extend our earlier work by analyzing more closely the issues involved in actually generating a contract execution(i.e., operationalization) that is beneficial and/or safe, i.e, correct, from a participantpsilas perspective. After doing so, we present an algorithm for semi-automatically generating such a family of safe and/or beneficial contract executions.