
TL;DR
The paper introduces tree buffers, a data structure that enables real-time monitors to produce error traces in runtime verification, and demonstrates their effectiveness in automata-based monitoring and regex capturing.
Contribution
It presents a novel data structure, tree buffers, with proven optimal bounds, to support real-time error trace generation in runtime verification and other domains.
Findings
Tree buffers enable real-time error trace generation in automata-based monitors.
Tree buffers are effective in capturing groups in regular expressions.
Empirical validation shows optimal performance in regex searching and runtime verification.
Abstract
In runtime verification, the central problem is to decide if a given program execution violates a given property. In online runtime verification, a monitor observes a program's execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to produce error traces, should a property violation be observed. In this paper we introduce a data structure, called tree buffer, that solves this problem in the context of automata-based monitors: If the monitor itself respects hard real-time constraints, then enriching it by tree buffers makes it possible to provide error traces, which are essential for diagnosing defects. We show that tree buffers are also useful in other application domains. For example, they can be used to implement…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Formal Methods in Verification · Parallel Computing and Optimization Techniques
