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

Aldizkaria:
Lecture Notes in Computational Science and Engineering

ISSN: 1439-7358

Argitalpen urtea: 2007

Alea: 4739 LNCS

Orrialdeak: 329-336

Mota: Artikulua

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

Beste argitalpen batzuk: Lecture Notes in Computational Science and Engineering

Lotura duten proiektuak

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

2006/00092/001

Laburpena

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.