Formal Reasoning on a Web Coordination System

  1. Mata, E.J. 1
  2. Álvarez, P. 2
  3. Bañares, J.A. 2
  4. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 Universidad de Zaragoza
    info

    Universidad de Zaragoza

    Zaragoza, España

    ROR https://ror.org/012a91z28

Revue:
Lecture Notes in Computational Science and Engineering

ISSN: 1439-7358

Année de publication: 2007

Volumen: 4739 LNCS

Pages: 329-336

Type: Article

beta Ver similares en nube de resultados
SCOPUS: 2-s2.0-38449101331 WoS: WOS:000251543000042 GOOGLE SCHOLAR

D'autres publications dans: Lecture Notes in Computational Science and Engineering

Projets liés

Sistemas de cálculo simbólico: nuevos desarrollos en topología algebráica y fiabilidad

2006/00092/001

Résumé

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.