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

Zeitschrift:
Lecture Notes in Computational Science and Engineering

ISSN: 1439-7358

Datum der Publikation: 2007

Ausgabe: 4739 LNCS

Seiten: 329-336

Art: Artikel

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

Andere Publikationen in: Lecture Notes in Computational Science and Engineering

Projekte im Zusammenhang

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

2006/00092/001

Zusammenfassung

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.