Distributed system contract monitoring

DOI10.1016/J.JLAP.2013.04.001MaRDI QIDQ2436454zbMATH OpenOpenAlexFDO

Authors Adrian Francalanza, Andrew Gauci, Gordon J. Pace

Publication date 25 February 2014

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

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

zbMATH Keywords

\({\pi}\)-calculusdistributed systemsmigrating monitorsruntime verification

Mathematics Subject Classification ID

Distributed systems (68M14) 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: The use of behavioural contracts, to specify, regulate and verify systems, is particularly relevant to runtime monitoring of distributed systems. System distribution poses major challenges to contract monitoring, from monitoring-induced information leaks to computation load balancing, communication overheads and fault-tolerance. We present mDPi, a location-aware process calculus, for reasoning about monitoring of distributed systems. We define a family of Labelled Transition Systems for this calculus, which allow formal reasoning about different monitoring strategies at different levels of abstractions. We also illustrate the expressivity of the calculus by showing how contracts in a simple contract language can be synthesised into different mDPi monitors.

Recommendations

• On distributed monitoring of asynchronous systems
• Decentralized asynchronous crash-resilient runtime verification
• Failure-aware runtime verification of distributed systems

Cited in

(17)

• Computer says no: verdict explainability for runtime monitors using a local proof system
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Precision, recall, and sensitivity of monitoring partially synchronous distributed programs
• A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring
• Monitorability for the Hennessy-Milner logic with recursion
• A theory of monitors (extended abstract)
• On distributed monitoring of asynchronous systems
• Counterexample guided synthesis of monitors for realizability enforcement
• Formalizing monitoring processes for large-scale distributed systems using abstract state machines
• Failure-aware runtime verification of distributed systems
• Decentralized runtime verification of message sequences in message-based systems
• Interaction-based offline runtime verification of distributed systems
• Runtime verification of partially-synchronous distributed system
• Organising LTL monitors over distributed systems with a global clock
• Centralized vs decentralized monitors for hyperproperties
• Centralized vs. decentralized monitors for hyperproperties
• Synthesising correct concurrent runtime monitors

This page was built for publication: Distributed system contract monitoring

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