Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible.The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time.
Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata.
Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
@inproceedings{grosen2025time,title={Time for Timed Monitorability},author={Grosen, Thomas M{\o}ller and Kauffman, Sean and Guldstrand Larsen, Kim and Zimmermann, Martin},booktitle={International Conference on Concurrency Theory {(CONCUR'25)}},origin={Professor},year={2025},month=aug,publisher={Schloss Dagstuhl - Leibniz-Zentrum für Informatik},isbn={978-3-95977-339-3},location={Aarhus, Denmark},note={Accepted},selected=true,preview=clock.webp}
We introduce a method for visualizing the temporal intervals output by nfer, a language and tool for event trace comprehension.
Visualizing these intervals is challenging because they may be arbitrarily nested in a hierarchy and because multiple intervals with the same identifier may occur concurrently.
Our tool, nvis, solves these problems to present the output of nfer in a human interpretable, interactive web interface.
We introduce an algorithm to solve the hierarchy and concurrency problem, and present a case study using automatically learned rules from our industrial partner.
@inproceedings{sadman2025visualizing,title={Visualizing Temporal Interval Hierarchies},author={Sadman, Nafiz and Kian Ersi, Nastaran and Kauffman, Sean},booktitle={{NASA} Formal Methods {(NFM'25)}},year={2025},month=jun,publisher={Springer},series={LNCS},volume={15682},isbn={978-3-031-93705-7},doi={10.1007/978-3-031-93706-4_19},location={Williamsburg, USA},selected=true,preview=nvis.svg}
Nfer is a Runtime Verification language for the analysis of event traces
that applies rules to create hierarchies of time intervals. This work
examines the complexity of the evaluation and satisfiability problems for
the data-free fragment of nfer. The evaluation problem asks whether a given
interval is generated by applying rules to a known input, while the
satisfiability problem asks if an input exists that will generate a given
interval.
By excluding data from the language, we achieve PTime complexity for the
evaluation problem and satisfiability when only considering inclusive rules,
and decidability for the satisfiability problem for cycle-free
specifications. Finally, we show that for the full data-free language,
satisfiability is undecidable.
@inproceedings{kauffman2024datafree,title={The Complexity of Data-Free Nfer},author={Kauffman, Sean and Guldstrand Larsen, Kim and Zimmermann, Martin},booktitle={International Conference on Runtime Verification (RV'24)},publisher={Springer},year={2024},month=oct,pages={174--191},series={LNCS},volume={15191},isbn={978-3-031-74233-0},doi={10.1007/978-3-031-74234-7_11},location={Instanbul, Turkey},selected=true,preview=rv24-logo.svg}
Annotating Control-Flow Graphs for Formalized Test Coverage Criteria
Control flow coverage criteria are an important part of the process of
qualifying embedded software for safety-critical systems. Criteria such
as modified condition/decision coverage (MC/DC) as defined by DO-178B are
used by regulators to judge the adequacy of testing and by QA engineers to
design tests when full path coverage is impossible.
Despite their importance, these coverage criteria are often misunderstood.
One problem is that their definitions are typically written in natural
language specification documents, making them imprecise. Other works have
proposed formal definitions using binary predicate logic, but these
definitions are difficult to apply to the analysis of real programs.
Control-Flow Graphs (CFGs) are the most common model for analyzing program
logic in compilers, and seem to be a good fit for defining and analyzing
coverage criteria. However, CFGs discard the explicit concept of a
decision, making their use for this task seem impossible.
In this paper, we show how to annotate a CFG with decision information
inferred from the graph itself. We call this annotated model a Control-
Flow Decision Graph (CFDG) and we use it to formally define several common
coverage criteria. We have implemented our algorithms in a tool which we
show can be applied to automatically annotate CFGs output from popular
compilers.
@inproceedings{kauffman2024annotating,title={Annotating Control-Flow Graphs for Formalized Test Coverage Criteria},author={Kauffman, Sean and Moreno, Carlos and Fischmeister, Sebastian},booktitle={International Conference on Software Testing, Verification and Validation Workshops (ICSTW'24)},year={2024},doi={10.1109/ICSTW60967.2024.00021},pages={{55-62}},publisher={IEEE},isbn={979-8-3503-4479-0},issn={2159-4848},location={Toronto, Canada},selected=true,preview=cfgd.svg,keywords={Control Flow Graphs, Test coverage criteria, Program modeling}}
Nfer is a rule-based language for abstracting event streams into a
hierarchy of intervals with data. Nfer has multiple implementations and has
been applied in the analysis of spacecraft telemetry and autonomous vehicle
logs. This work provides the first complexity analysis of nfer evaluation,
i.e., the problem of deciding whether a given interval is generated by
applying rules. We show that the full nfer language is undecidable and that
this depends on both recursion in the rules and an infinite data domain. By
restricting either or both of those capabilities, we obtain tight
decidability results. We also examine the impact on complexity of exclusive
rules and minimality. For the most practical case, which is minimality with
finite data, we provide a polynomial-time algorithm.
@article{kauffman2024complexity,title={The Complexity of Evaluating nfer},author={Kauffman, Sean and Zimmermann, Martin},journal={Science of Computer Programming},volume={231},year={2024},issn={0167-6423},doi={10.1016/j.scico.2023.103012},selected=true,preview=scp-journal.jpg,keywords={Interval logic, Complexity, Runtime verification}}
