Gerardo Schneider, Researcher, University of Oslo
In this talk I will describe CL, a formal language for writing (electronic) contracts, in the context of Service-Oriented Architectures (SOA). The language allows to write (conditional) obligations, permissions and prohibitions, and to represent the so-called contrary-to-duties (CTDs) and contrary-to-prohibitions (CTPs). CTDs and CTPs are useful to establish what happen in case obligations, respectively prohibitions, are not respected. The approach is action-based, meaning that the above normative notions are defined on actions and not on state-of-affairs. I will then sketch some initial ideas on model checking contracts as well as recent work on automatic extraction of contract monitors. Finally, I will present some open problems, and other application domains of CL, besides SOA.