Protocol specification and verification by using computational logic

The aim of this paper is to report on some preliminary results obtained in the context of the MASSIVE research project (http://www.di.unito.it/massive/) relating the formal specification and verification of protocols in some different application field. A protocol is a way to express the right behavior of entities involved in a (possibly complex and distributed) process. The formalism to be used for protocol description should be as intuitive as possible, but it should be also formally defined, in order to allow formal checks both on the features of the protocol itself (e.g. termination), and also on the execution of it. To this purpose, we will show some results obtained by exploiting the SOCS ¡ SI logic-based framework for the specification and the verification of protocols in various applicative fields such as electronic commerce, medicine and elearning. We will also present a new graphical notation to express medical guidelines, which could be automatically translated into the SOCS formalism.