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

distributed systemsruntime verification\({\pi}\)-calculusmigrating monitors

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) 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

(15)

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

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)