This book presents a set of 8 papers accompanying the lectures of leading researchers given at the 9th edition of the International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2009, held in Bertinoro, Italy, in June 2009. SFM 2009 was devoted to formal methods for web services and covered several aspects including coreography, orchestration, description techniques, interaction, synthesis, composition, session types, contracts, verification, security, and performance.
Author(s): Marco Bernardo, Luca Padovani, Gianluigi Zavattaro
Edition: 1
Year: 2009
Language: English
Pages: 348
Behavioural Contracts......Page 7
Introduction......Page 1
Notation......Page 2
SRMC......Page 3
Contracts: Syntax and Semantics......Page 5
Workflow Patterns Initiative......Page 6
Service Discovery......Page 12
Deduction System for the Weak Subcontract Relation......Page 16
Namespace Scoping......Page 19
Rate Parameter Experiments......Page 22
Query Specification......Page 23
Contract Duality with Orchestration......Page 26
Refining Services......Page 29
Application Example......Page 31
Large-Scale Modelling with Differential Equations......Page 32
Related and Future Work......Page 33
{ f smc}......Page 36
Conclusion and Future Perspectives......Page 37
References......Page 48
Synchronous Orchestrators......Page 10
Recursive Types......Page 14
Uncertainty about Parameters......Page 15
Uncertainty about System Configurations......Page 17
Namespace Selections......Page 20
Algorithmic Type Checking......Page 21
Detailed Comparison with Our Previous Work......Page 25
{ f Pepato}......Page 35
Encoding an SEA as an Engine......Page 39
Service Graphs as STS......Page 41
A.3 Proofs of §4......Page 42
Data Nets as STS......Page 43
Generating the Composite Service......Page 44
References......Page 95
Related Work......Page 4
Case Study......Page 8
Interpretations of Synchronous Orchestrators......Page 18
Interactional Exceptions......Page 24
Markovian Modelling with Many Models......Page 28
Planning in Asynchronous Domains......Page 38
A Detailed Results......Page 40
The ASTRO WS-Compose Tool......Page 45
A.5 Proofs of §7......Page 47
{ f WS-Synth}: An Overview of the Tool......Page 49
The Amazon-MPS Composition Domain......Page 51
The Amazon-MPS Composition Requirements......Page 59
Generating the e-Bookstore Executable Process......Page 63
Concluding Remarks......Page 64
References......Page 164
References......Page 193
Subcontract Pre-orders as Correctness Preserving Refinements......Page 13
References......Page 219
A Process Algebraic Representation of Contracts......Page 27
B Proof of Proposition 3......Page 30
A.4 Proofs of §5......Page 46
References......Page 267
Initial Performance Model......Page 9
References......Page 302
