Abstract
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). © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Mata, E. J., Álvarez, P., Bañares, J. A., & Rubio, J. (2007). Formal reasoning on a Web coordination system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4739 LNCS, pp. 329–336). Springer Verlag. https://doi.org/10.1007/978-3-540-75867-9_42
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
