Formal modelling and verification in service-oriented computing

Formal methods and tools are a popular means of analysing the correctness properties of computer network protocols, such as safety, liveness and security. First the protocol under scrutiny is described in a formal language, which often results in a more precise definition of its function. Subsequently, the properties to be analysed are specified in a suitable logic. Finally, to decide whether or not the protocol fulfils certain properties, automatic tools are used to analyse it. The outcome either proves the protocol to be correct with respect to the relevant properties or shows there to be a problem.