We tackle the problem of providing rigorous formal foundations to current software engineering technologies for web services, and especially to WSDL and WS-BPEL, two of the most used XML-based standard languages for web services. We focus on a simplified fragment of WS-BPEL sufficiently expressive to model asynchronous interactions among web services in a network context. We present this language as a process calculus-like formalism, that we call WS-CALCULUS, for which we define an operational semantics and a type system. The semantics provides a precise operational model of programs, while the type system forces a clean programming discipline for integrating collaborating services. We prove that the operational semantics of WS-CALCULUS and the type system are ‘sound’ and apply our approach to some illustrative examples. We expect that our formal development can be used to make the relationship between WS-BPEL programs and the associated WSDL documents precise and to support verification of their conformance.
A WSDL-based type system for asynchronous WS-BPEL processes / A.Lapadula; R.Pugliese; F.Tiezzi. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 1572-8102. - STAMPA. - 38(2):(2011), pp. 119-157. [10.1007/s10703-010-0110-0]
A WSDL-based type system for asynchronous WS-BPEL processes
PUGLIESE, ROSARIO;F. Tiezzi
2011
Abstract
We tackle the problem of providing rigorous formal foundations to current software engineering technologies for web services, and especially to WSDL and WS-BPEL, two of the most used XML-based standard languages for web services. We focus on a simplified fragment of WS-BPEL sufficiently expressive to model asynchronous interactions among web services in a network context. We present this language as a process calculus-like formalism, that we call WS-CALCULUS, for which we define an operational semantics and a type system. The semantics provides a precise operational model of programs, while the type system forces a clean programming discipline for integrating collaborating services. We prove that the operational semantics of WS-CALCULUS and the type system are ‘sound’ and apply our approach to some illustrative examples. We expect that our formal development can be used to make the relationship between WS-BPEL programs and the associated WSDL documents precise and to support verification of their conformance.File | Dimensione | Formato | |
---|---|---|---|
11FMSD-A WSDL-based type system for asynchronous WS-BPEL processes.pdf
Accesso chiuso
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Tutti i diritti riservati
Dimensione
1.15 MB
Formato
Adobe PDF
|
1.15 MB | Adobe PDF | Richiedi una copia |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.