Runtime verification (RV) consists of verifying that an execution trace satisfies a specification. The specification can be written in a formal logic, or it can be written as code in a general purpose programming language. In this paper we present an RV method, and a corresponding tool, that explores the boundary between formal logic and general purpose programming. The tool, called PyDejaVu, supports a two-phase approach to writing properties, where a property can be expressed in a combination of an operational phase and a declarative phase. The operational phase is expressed in an internal Python DSL (Domain-Specific Language), whereas the declarative phase is expressed in the external DSL Qtl (Quantified Temporal Logic) for first-order past time temporal logic. This approach benefits from the expressiveness of Python and the succinctness and efficiency of monitoring Qtl. Our tool builds on the previous runtime verification tool DejaVu monitoring Qtl properties.

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

Embedding Monitoring of First-Order Temporal Logic in a Programming Language

  • Klaus Havelund,
  • Moran Omer,
  • Doron Peled

摘要

Runtime verification (RV) consists of verifying that an execution trace satisfies a specification. The specification can be written in a formal logic, or it can be written as code in a general purpose programming language. In this paper we present an RV method, and a corresponding tool, that explores the boundary between formal logic and general purpose programming. The tool, called PyDejaVu, supports a two-phase approach to writing properties, where a property can be expressed in a combination of an operational phase and a declarative phase. The operational phase is expressed in an internal Python DSL (Domain-Specific Language), whereas the declarative phase is expressed in the external DSL Qtl (Quantified Temporal Logic) for first-order past time temporal logic. This approach benefits from the expressiveness of Python and the succinctness and efficiency of monitoring Qtl. Our tool builds on the previous runtime verification tool DejaVu monitoring Qtl properties.