Embedding Runtime Verification in Python

Runtime verification consists of verifying that an execution trace satisfies a specification. The specification can be formal, but it can also be informal, e.g. code in a general purpose programming language. In this paper we present the tool PyDejaVu, which explores the boundary between general purpose programming and formal specification. The tool 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. The tool builds on the previous runtime verification tool DejaVu monitoring Qtl properties, and is compared with the previous TP-DejaVu tool, which supports a purely external DSL for two-phase runtime verification.