Monitorability of contracts for web services

Abstract

Web services typically consist of two types of components, servers and clients, which interact with each other through service interactions. A server can be seen as a collection of services that a client invokes in order to reach a successful state. A server can be described in terms of a contract, which defi nes the service interactions that it offers. Dually, a client may also be portrayed by a contract, describing sequences of interactions that it expects to conduct with a server. In a dynamic service discovery setting, where clients search for compatible services with whom to interact, a server contract may be advertised by a server as its specification. A server may inadvertently or maliciously advertise a contract which it does not implement. Although static-based techniques can be employed to verify whether a server actually implements its advertised contract or not, there are settings where static verifi cation cannot be used. Furthermore, a client may decide not to trust a server. In such cases, the client is forced to verify the behaviour of the server at runtime. This scenario may be viewed as an instance of Runtime Veri fication, where a pertinent question is whether contracts can be monitored for adequately at runtime, otherwise stated as the monitorability of contracts. In general, not all specifications can be verified in a correct manner at runtime. In this dissertation, we set up to investigate this problem. We consider a language of contracts describing both clients and servers, together with a formal notion of \agreement" amongst these two types of contracts. We then develop a formal monitoring framework where we instrument servers with our monitors. We de fine monitor properties that relate monitors to server specifications that are de fined using contracts. One such property determines whether the conclusion reached by a monitor is correct wrt. a specification contract. Another property states that a monitor must be able to reach a conclusion about the server. In other words, it must be able to tell whether the server is implementing a specification or not. These properties are then used to study the notion of monitorability of contracts by using the newly created monitor language to defi ne an automatic synthesis from contracts to monitors. By using this synthesis, we show whether our contract language can create monitors which satisfy these properties.