Titlebook: Runtime Verification; 19th International C Bernd Finkbeiner,Leonardo Mariani Conference proceedings 2019 Springer Nature Switzerland AG 201

enumaerate

通情达理

Explaining Violations of Properties in Control-Flow Temporal Logic,mented as an extension to the publicly available . tool. Our work is motivated by results obtained applying . to a web service on the CMS Experiment at CERN and initial tests produce useful explanations for realistic use cases.

虚度

An Extension of LTL with Rules and Its Application to Runtime Verification,eficiencies of first-order LTL and suggest an extension of (propositional as well as first-order) LTL with rules to address these limitations. We describe how the . tool is correspondingly extended and provide some experimental results.

flourish

Camouflage

On the Runtime Enforcement of Timed Properties,med automata and feature uncontrollable events. Then, we mention some tools capable of runtime enforcement, and we present the TiPEX tool dedicated to timed properties. Finally, we present some open challenges and avenues for future work.

MENT

Algorithms for Monitoring Hyperproperties,ization techniques for keeping the execution trace storage and algorithmic workload as low as possible and also report on experiments run on the combinatorial as well as the constraint-based monitoring algorithms.

refraction

Dungeon

Monitorability over Unreliable Channels,ts on program monitoring. We propose a fixed-parameter tractable algorithm for determining the immunity of a finite automaton to a trace mutation and show how it can be used to classify .-regular properties as monitorable over channels with that mutation.

国家明智

A Retrospective Look at the Monitoring and Checking (MaC) Framework,ame to be known as runtime verification. The project also built a pioneering runtime verification tool, Java-MaC, that was an instantiation of the approach to check properties of Java programs. In this retrospective, we discuss decisions made in the design of the framework and summarize lessons lear

separate

Introspective Environment Modeling,ts in the environment can be hard to predict, let alone their behavior. We present the idea of ., in which one algorithmically synthesizes, by introspecting on the system, assumptions on the environment under which the system can guarantee correct operation and which can be efficiently monitored at