Abstract
Requirements on message-based interactions can be formalised as an interface contract that specifies constraints on the sequence of possible messages that can be exchanged by multiple parties. At runtime, each peer can monitor incoming messages and check that the contract is correctly being followed by their respective senders. We introduce cooperative runtime monitoring, where a recipient ‘delegates’ its monitoring task to the sender, which is required to provide evidence that the message it sends complies with the contract. In turn, this evidence can be quickly checked by the recipient, which is then guaranteed of the sender's compliance to the contract without doing the monitoring computation by itself. A particular application of this concept is shown on web services, where service providers can monitor and enforce contract compliance of third-party clients at a small cost on the server side, while avoiding to certify or digitally sign them.
Notes
1. Remark that all witnesses must be kept, since the validity of the next message requires that any one of them spawns a non- ⊥ node in the next round of decomposition.
2. The source code of the runtime monitor, including proof validation methods, can be found at http://beepbeep.sourceforge.net.