Runtime Verification (RV) allows monitoring the behaviors of a system while checking them against a formal specification. The executions of distributed systems are often modeled using interleaving semantics, where events of different processes are interleaved into a total order. However, certain behavioral properties are difficult to express using interleaving semantics, whereas they can be naturally expressed in terms of partial order semantics. We study the problem of runtime verification for distributed systems based on the global states structure associated with a partial order execution. We present two algorithms for RV with branching temporal specifications and study the complexity of this problem. The first algorithm is for a global temporal logic with past operators we term PaCTL (for Past CTL). It involves constructing the branching structure of global states. We then show a second, more efficient, algorithm, for a subset of this logic that we term PaBTL. This algorithm does not require constructing the branching structure. We present implementations for both algorithms with experimental results.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Monitoring Distributed Systems Based on Partial Order Executions with Global States

  • Moran Omer,
  • Doron Peled,
  • Ely Porat,
  • Vijay K. Garg

摘要

Runtime Verification (RV) allows monitoring the behaviors of a system while checking them against a formal specification. The executions of distributed systems are often modeled using interleaving semantics, where events of different processes are interleaved into a total order. However, certain behavioral properties are difficult to express using interleaving semantics, whereas they can be naturally expressed in terms of partial order semantics. We study the problem of runtime verification for distributed systems based on the global states structure associated with a partial order execution. We present two algorithms for RV with branching temporal specifications and study the complexity of this problem. The first algorithm is for a global temporal logic with past operators we term PaCTL (for Past CTL). It involves constructing the branching structure of global states. We then show a second, more efficient, algorithm, for a subset of this logic that we term PaBTL. This algorithm does not require constructing the branching structure. We present implementations for both algorithms with experimental results.