Optimal Runtime Verification of Finite State Properties over Lossy Event Streams

Stream Runtime Monitoring on UAS

Unmanned Aircraft Systems (UAS) with autonomous decision-making capabilities are of increasing interest for a wide area of applications such as logistics and disaster recovery. In order to ensure the correct behavior of the system and to recognize hazardous situations or system faults, we applied stream runtime monitoring techniques within the DLR ARTIS (Autonomous Research Testbed for Intelligent System) family of unmanned aircraft. We present our experience from specification elicitation, instrumentation, offline log-file analysis, and online monitoring on the flight computer on a test rig. …

POLIMON：在运行时检查乱序流上的时间属性

POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime

本文提出运行时监控工具POLIMON，通过MTL及其冻结量词扩展规约检查系统行为，支持接收并立即处理乱序消息以迅速输出违规判定，适用于验证具有不可靠通道的分布式系统。

Runtime Verification over Out-of-order Streams

We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where messages can be delayed, reordered, or even lost. Furthermore, our approach handles an expressive specification language that extends the real-time logic MTL with freeze quantifiers for reasoning about data values. The logic's main novelty is a new three-valued semantics that is well suited for runtime verification as it accounts for partial knowledge about a system's behavior. Based on this semantics, we present online alg…

Runtime Verification For Timed Event Streams With Partial Information

Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real-world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abs…

Runtime Verification of Temporal Properties over Out-of-order Data Streams

We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messages can be delayed or lost. In contrast to prior works, whose property specification languages are limited to propositional temporal logics, our approach handles an extension of the real-time logic MTL with freeze quantifiers for reasoning about data values. We present its underlying theory based on a new three-valued semantics that is well suited to soundly and completely reason online about event streams in the pre…

LOLA中运行时验证与基于模型诊断的统一框架

A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA

提出在流规范语言LOLA中统一运行时验证与基于模型诊断的框架，通过将系统描述、组件健康状态和观测编码为单一流形式，实现在线故障定位。