Counterexample guided synthesis of monitors for realizability enforcement

DOI10.1007/978-3-642-33386-6_20MaRDI QIDQ4649300zbMATH OpenOpenAlexFDO

Authors Matthias Güdemann, Gwen Salaün, Meriem Ouederni

Publication date 21 November 2012

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33386-6_20

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

• Deciding choreography realizability
• Distributed system contract monitoring
• Conversation protocols: a formalism for specification and verification of reactive electronic services
• Conversation protocols: a formalism for specification and verification of reactive electronic services
• Automated synthesis of distributed controllers

Cited in

(5)

• Automated verification of automata communicating via FIFO and bag buffers
• Automatic analysis of complex interactions in microservice systems
• Runtime enforcement with reordering, healing, and suppression
• Unreliability in practical subclasses of communicating systems
• Realizable temporal logics for web service choreography

Describes a project that uses

Uses Software

• LNT2LOTOS
• CADP
• XTL

This page was built for publication: Counterexample guided synthesis of monitors for realizability enforcement

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