Dmitriy Traytel

Last Name

Traytel

First Name

Dmitriy

ORCID

0000-0001-7982-2768

Show all metadata

Search Results

Publications 1 - 10 of 32

Explainable Online Monitoring of Metric Temporal Logic
Lima, Leonardo; Herasimau, Andrei; Raszyk, Martin; et al. (2023)
Lecture Notes in Computer Science ~ Tools and Algorithms for the Construction and Analysis of Systems
Runtime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor's user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.
A Formally Verified Monitor for Metric First-Order Temporal Logic
Schneider, Joshua; Basin, David; Krstić, Srđan; et al. (2019)
Lecture Notes in Computer Science ~ Runtime Verification
A survey of challenges for runtime verification from advanced application domains (beyond software)
Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; et al. (2019)
Formal Methods in System Design
Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.
A Taxonomy for Classifying Runtime Verification Tools
Falcone, Yliès; Krstić, Srđan; Reger, Giles; et al. (2018)
Lecture Notes in Computer Science ~ Runtime Verification: 18th International Conference, RV 2018 Limassol, Cyprus, November 10–13, 2018: Proceedings
Scalable Online First-Order Monitoring
Schneider, Joshua; Basin, David; Brix, Frederik; et al. (2018)
Lecture Notes in Computer Science ~ Runtime Verification: 18th International Conference, RV 2018 Limassol, Cyprus, November 10–13, 2018: Proceedings
Correct and Efficient Policy Monitoring, a Retrospective
Basin, David; Krstić, Srđan; Schneider, Joshua; et al. (2023)
Lecture Notes in Computer Science ~ Automated Technology for Verification and Analysis
The MonPoly project started over a decade ago to build effective tools for monitoring trace properties, including functional correctness, security, and compliance policies. The original MonPoly tool supported monitoring specifications given in metric first-order temporal logic, an expressive specification language. It handled both the online case, where system events are monitored as they occur, and the offline case, monitoring logs. Our tool has evolved over time into a family of tools and supporting infrastructure to make monitoring both scalable and suitable for high assurance applications. We survey this evolution which includes: (1) developing more expressive monitors, e.g., adding aggregation operators, regular expressions, and limited forms of recursion; (2) delimiting efficiently monitorable fragments and designing new monitoring algorithms for them; (3) supporting parallel and distributed monitoring; (4) using theorem proving to verify monitoring algorithms and explore extensions; and (5) carrying out ambitious case studies.
Verified First-Order Monitoring with Recursive Rules
Zingg, Sheila; Krstić, Srđan; Raszyk, Martin; et al. (2022)
Lecture Notes in Computer Science ~ Tools and Algorithms for the Construction and Analysis of Systems
First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let’s usefulness on several example specifications and evaluate our verified algorithm’s performance against the DejaVu monitoring tool.
Optimal Proofs for Linear Temporal Logic on Lasso Words
Basin, David; Bhatt, Bhargav Nagaraja; Traytel, Dmitriy (2018)
Lecture Notes in Computer Science ~ Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings
Proactive Real-Time First-Order Enforcement
Hublet, François; Lima, Leonardo; Basin, David; et al. (2024)
Lecture Notes in Computer Science ~ Computer Aided Verification
Modern software systems must comply with increasingly complex regulations in domains ranging from industrial automation to data protection. Runtime enforcement addresses this challenge by empowering systems to not only observe, but also actively control, the behavior of target systems by modifying their actions to ensure policy compliance. We propose a novel approach to the proactive real-time enforcement of policies expressed in metric first-order temporal logic (MFOTL). We introduce a new system model, define an expressive MFOTL fragment that is enforceable in that model, and develop a sound enforcement algorithm for this fragment. We implement this algorithm in a tool called WhyEnf and carry out a case study on enforcing GDPR-related policies. Our tool can enforce all policies from the study in real-time with modest overhead. Our work thus provides the first tool-supported approach that can proactively enforce expressive first-order policies in real time.
Adaptive Online First-Order Monitoring
Schneider, Joshua; Basin, David; Brix, Frederik; et al. (2019)
Lecture Notes in Computer Science ~ Automated Technology for Verification and Analysis

Publications 1 - 10 of 32

Dmitriy Traytel

Last Name

First Name

ORCID

Organisational unit

Filters

Search Results