Formal Reasoning on a Web Coordination System

摘要

In this paper, a first step toward the use of Artificial Intelligence tools (namely proof assistants) in the formal analysis of programs for Web services coordination is presented. This first attempt consists in the formal modeling of a system with transactional capabilities. The model is devised on a variant of the well-known Linda model for generative communication. We explore then the role of the Rete algorithm to implement efficiently a transactional read operation, opening the way for a further formal analysis of it, by means of automated testing against a certified program (i.e. a program verified with the help of a proof assistant).