Automata for Specifying and Orchestrating Service Contracts

DOI10.2168/LMCS-12(4:6)2016MaRDI QIDQ2974790zbMATH OpenFDO

Authors D. Basile, Pierpaolo Degano, Gian Luigi Ferrari

Publication date 11 April 2017

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1607.08363

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.

Recommendations

• Automata for analysing service contracts
• From orchestration to choreography through contract automata
• Parametrized automata simulation and application to service composition
• Contract-Directed Synthesis of Simple Orchestrators
• A contract language for service-oriented dynamic collaborations
• Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition

Cited in

(12)

• Transactions and contracts based on reaction systems
• A verification-driven framework for iterative design of controllers
• Relating two automata-based models of orchestration and choreography
• Automata for analysing service contracts
• Contract-Directed Synthesis of Simple Orchestrators
• Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services
• From orchestration to choreography through contract automata
• Can we communicate? Using dynamic logic to verify team automata
• Research Challenges in Orchestration Synthesis
• Advancing orchestration synthesis for contract automata
• Formal analysis of the contract automata runtime environment with \textsc{Uppaal}: modelling, verification and testing
• Contract-based discovery of Web services modulo simple orchestrators

This page was built for publication: Automata for Specifying and Orchestrating Service Contracts

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974790)