Realizable temporal logics for web service choreography

DOI10.1016/J.JLAMP.2016.06.002MaRDI QIDQ739636zbMATH OpenOpenAlexFDO

Authors D. Kharzeev

Publication date 18 August 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2016.06.002

zbMATH Keywords

formal methodsweb serviceschoreographycommunicating automatalocal temporal logics

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Internet topics (68M11)

Recommendations

• Analysis of Realizability Conditions for Web Service Choreographies
• Deciding choreography realizability
• Realizability and dynamic reconfiguration of chor specifications
• The semantics and verification of timed service choreography
• Realisability of choreographies

Cites work

• scientific article; zbMATH DE number 1670846 (Why is no real title available?)
• An expressively complete linear time temporal logic for Mazurkiewicz traces
• Analysis of Realizability Conditions for Web Service Choreographies
• Conversation protocols: a formalism for specification and verification of reactive electronic services
• Counterexample guided synthesis of monitors for realizability enforcement
• Deciding choreography realizability
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Formal Models of Communicating Systems
• Mathematical Foundations of Computer Science 2003
• On Communicating Finite-State Machines
• Realizability and verification of MSC graphs
• Reasoning about layered message passing systems
• Structured Communication-Centred Programming for Web Services

Cited in

(13)

• Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services
• Event-B-supported choreography-defined communicating systems
• Analysis of Realizability Conditions for Web Service Choreographies
• Realizable causal-consistent reversible choreographies for systems with first-in-first-out communication channels
• A centralized and a decentralized method to automatically derive choreography-conforming web service systems
• A dynamic temporal logic for quality of service in choreographic models
• Realizability and dynamic reconfiguration of chor specifications
• Analyzing Chor specifications by translation into FSP
• Resolving non-determinism in choreographies
• Conversation protocols: a formalism for specification and verification of reactive electronic services
• The semantics and verification of timed service choreography
• Conversation protocols: a formalism for specification and verification of reactive electronic services
• Declarative choreographies and liveness

This page was built for publication: Realizable temporal logics for web service choreography

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