Abstract | Interaction in both agent-based and component-based architectures is facilitated by sharable, verified and unambiguous protocols with desirable properties. An interaction protocol may be expressed as a logical theory e.g. dynamic logic, joint intention theory or event calculus, thereby enabling the proof of its properties and its correctness. This paper focuses on new joint work in specifying and proving properties such as safety and liveness, of interaction protocols, in componentbased frameworks. A safe and sound interaction allows no unpredictable states and transitions, and states allowed for the behaviour are only those that are defined by the protocol. Other properties such as termination, soundness, completeness, stability and fairness can be specified and verified for such protocols. |
---|