Event-B-supported choreography-defined communicating systems

DOI10.1007/978-3-030-48077-6_11MaRDI QIDQ5040369zbMATH OpenOpenAlexFDO

Authors Sarah Benyagoub, Yamine Ait-Ameur, Klaus-Dieter Schewe

Publication date 14 October 2022

Published in Rigorous State-Based Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-48077-6_11

zbMATH Keywords

choreographycompleteness proofcorrectness proofEvent-Brealisability

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Realisability of choreographies
• Compositional choreographies
• Deciding choreography realizability
• Realizable causal-consistent reversible choreographies for systems with first-in-first-out communication channels
• Realizable temporal logics for web service choreography

Cites work

• Decidable topologies for communicating automata with FIFO and bag channels
• Deciding choreography realizability
• Mixing Lossy and Perfect Fifo Channels
• On Communicating Finite-State Machines
• On deciding synchronizability for asynchronously communicating systems
• Realisability of choreographies

Cited in

(1)

• Realizable causal-consistent reversible choreographies for systems with first-in-first-out communication channels

This page was built for publication: Event-B-supported choreography-defined communicating systems

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