@article{kauffman2024complexity,
title = {The Complexity of Evaluating nfer},
author = {Sean Kauffman and Martin Zimmermann},
journal = {Science of Computer Programming},
origin = {Postdoc},
volume = {231},
year = {2024},
issn = {0167-6423},
doi = {10.1016/j.scico.2023.103012},
abstract = {
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.
},
keywords = {Interval logic, Complexity, Runtime verification}
}
@inproceedings{dierl2023learning,
title={Learning Symbolic Timed Models from Concrete Timed Data},
author={Dierl, Simon and Howar, Falk Maria and Kauffman, Sean
and Kristjansen, Martin and Guldstrand Larsen, Kim and Lorber, Florian
and Mauritz, Malte},
booktitle={{NASA} Formal Methods (NFM'23)},
origin={Postdoc},
year={2023},
month={06},
pages={104--121},
publisher={Springer},
doi={10.1007/978-3-031-33170-1_7},
isbn={978-3-031-33170-1},
series={LNCS},
volume={13903},
abstract={
We present a technique for learning explainable timed automata
from passive observations of a black-box function, such as an artificial
intelligence system. Our method accepts a single, long, timed word with
mixed input and output actions and learns a Mealy machine with one timer.
The primary advantage of our approach is that it constructs a symbolic
observation tree from a concrete timed word. This symbolic tree is then
transformed into a human comprehensible automaton. We provide a prototype
implementation and evaluate it by learning the controllers of two systems:
a brick-sorter conveyor belt trained with reinforcement learning and a
real-world derived smart traffic light controller. We compare different
model generators using our symbolic observation tree as their input and
achieve the best results using k-tails. In our experiments, we learn
smaller and simpler automata than existing passive timed learners while
maintaining accuracy.
}
}
@article{kauffman2023software,
title = {Log Analysis and System Monitoring with nfer},
author = {Kauffman, Sean},
journal = {Science of Computer Programming},
publisher = {Elsevier},
volume = {225},
year = {2023},
month = {01},
issn = {0167-6423},
doi = {10.1016/j.scico.2022.102909},
abstract = {
Nfer is a tool that implements the eponymous language for log analysis and
monitoring. Users write rules to calculate new information from an event
stream such as a program log either offline or online. In addition to a
command-line program, nfer exposes interfaces in Python and R and can
generate monitors for embedded systems. Nfer is designed to be fast and has
been repeatedly demonstrated to outperform similar tools.
},
keywords = {Log Analysis, Runtime Verification, Trace Abstraction}
}
@inproceedings{dams2022documentation,
title = {Runtime Verification as Documentation},
author = {Dams, Dennis and Havelund, Klaus and Kauffman, Sean},
booktitle = {International Symposium on Leveraging Applications
of Formal Methods (ISoLA'22)},
series = {LNCS},
volume = {13702},
publisher = {Springer},
year = {2022},
month = {10},
pages = {157--173},
doi = {10.1007/978-3-031-19756-7_9},
isbn = {978-3-031-19756-7},
abstract = {
In runtime verification, a monitor is used to return a Boolean verdict
on the behavior of a system. We present several examples of the use of
monitors to instead document system behavior. In doing so, we demonstrate
how runtime verification can be combined with techniques from data science
to provide novel forms of program analysis.
}
}
@inproceedings{dams2022pycontract,
title = {A Python Library for Trace Analysis},
author = {Dams, Dennis and Havelund, Klaus and Kauffman, Sean},
booktitle = {International Conference on Runtime Verification (RV'22)},
publisher = {Springer},
year = {2022},
month = {09},
pages = {264--273},
doi = {10.1007/978-3-031-17196-3_15},
isbn = {978-3-031-17196-3},
abstract = {
We present a Python library for trace analysis named PyContract. PyContract
is a shallow internal DSL, in contrast to many trace analysis tools that
implement external or deep internal DSLs. The library has been used in a
project for analysis of logs from NASA's Europa Clipper mission. We
describe our design choices, explain the API via examples, and present an
experiment comparing PyContract against other state-of-the-art tools from
the research and industrial communities.
}
}
@inproceedings{
grosen2022timed,
title = {Monitoring Timed Properties (Revisited)},
author = {Grosen, Thomas M{\o}ller and Kauffman, Sean and Larsen, Kim Guldstrand
and Zimmermann, Martin},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS'22)},
series = {LNCS},
volume = {13465},
publisher = {Springer},
year = {2022},
month = {08},
day = {29},
doi = {10.1007/978-3-031-15839-1_3},
pages = {43--62},
isbn = {978-3-031-15839-1},
abstract = {
In this paper we revisit monitoring real-time systems with respect to
properties expressed either in Metric Interval Temporal Logic or as Timed
B{\"u}chi Automata. We offer efficient symbolic online monitoring
algorithms in a number of settings, exploiting so-called zones well-known
from efficient model checking of Timed Automata. The settings considered
include new, much simplified treatment of time divergence, monitoring under
timing uncertainty, and, extension of monitoring to offer minimum time
estimates before conclusive verdicts can be made.
},
keywords = {Monitoring, Timed Automata, Metric Temporal Logic}
}
@inproceedings{kauffman2022complexity,
title = {The Complexity of Evaluating nfer},
author = {Kauffman, Sean and Zimmermann, Martin},
booktitle = {International Symposium on Theoretical Aspects of Software
Engineering (TASE'22)},
series = {LNCS},
volume = {13299},
publisher = {Springer},
year = {2022},
month = {07},
day = {03},
doi = {10.1007/978-3-031-10363-6_26},
pages = {388--405},
isbn = {978-3-031-10363-6},
issn = {0302-9743},
abstract = {
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.
},
keywords = {Interval logic, Complexity, Runtime verification}
}
@inproceedings{kauffman2021nfer,
title = {nfer -- A Tool for Event Stream Abstraction},
author = {Kauffman, Sean},
booktitle = {International Conference on Software Engineering and Formal
Methods (SEFM'21)},
series = {LNCS},
volume = {13085},
publisher = {Springer},
year = {2021},
isbn = {978-3-030-92124-8},
pages = {103--109},
doi = {10.1007/978-3-030-92124-8_6},
abstract = {
This work describes nfer, an open-source tool for event-stream abstraction
and processing. Nfer implements the Runtime Verification logic of the same
name, providing programming interfaces in C, R, and Python. Rules that
dictate nfer's behavior can be written in an external Domain-Specific
Language (DSL), mined from historical traces, or given using an internal
DSL in Python. The tool is designed for efficient online monitoring of
event streams and can also operate as an offline tool to process completed
logs.
}
}
@article{kauffman2021what,
author = {Kauffman, Sean and Havelund, Klaus and Fischmeister, Sebastian},
title = {What Can We Monitor Over Unreliable Channels?},
journal = {International Journal on Software Tools for Technology Transfer},
year = {2021},
month = {06},
day = {30},
pages = {579--600},
volume = {23},
issue = {4},
doi = {10.1007/s10009-021-00625-z},
issn = {1433-2779},
abstract = {
This article addresses the question of what properties can be monitored
over an unreliable communication channel. We model unreliable
communications as mutations to finite traces and define what it means
for a property to be immune to such a mutation. We also introduce the
idea of a trustworthy verdict, which is a verdict guaranteed to be correct
in the presence of a trace mutation. We show that the trustworthiness of
a verdict or immunity of a property for a single mutation is equivalent
to the trustworthiness or immunity for any number of mutations. We
classify trustworthy verdicts on $\omega$-regular properties by updating
a recently proposed monitorability-focused refinement of the safety-liveness
taxonomy. The article also includes a fixed-parameter tractable algorithm
to test an $\omega$-regular property for immunity to a trace mutation. Our
results show that many of the most common properties can be monitored over
unreliable channels.
}
}
@article{kauffman2021palisade,
title = {Palisade: A framework for anomaly detection in embedded systems},
author = {Kauffman, Sean and Dunne, Murray and Gracioli, Giovani
and Khan, Waleed and Benann, Nirmal and Fischmeister, Sebastian },
journal = {Journal of Systems Architecture},
year = {2021},
numpages = {17},
issn = {1383-7621},
doi = {10.1016/j.sysarc.2020.101876},
publisher = {Elsevier},
volume = {113},
pages = {101876},
abstract = {In this article, we propose Palisade, a distributed
framework for streaming anomaly detection. Palisade is motivated by
the need to apply multiple detection algorithms for distinct anomalies
in the same scenario. Our solution blends low latency detection with
deployment flexibility and ease-of-modification. This work includes a
thorough description of the choices made in designing Palisade and the
reasons for making those choices. We carefully define symptoms of
anomalies that may be detected, and we use this taxonomy in
characterizing our work. The article includes two case studies using a
variety of anomaly detectors on streaming data to demonstrate the
effectiveness of our approach in an embedded setting.
},
keywords = {Anomaly detection, Real-time embedded systems,
Software architecture, Streaming-based architecture}
}
@inproceedings{kauffman2019monitorability,
title = {Monitorability Over Unreliable Channels},
author = {Kauffman, Sean and Havelund, Klaus and Fischmeister, Sebastian},
booktitle = {International Conference on Runtime Verification (RV'19)},
series = {LNCS},
volume = {11757}
publisher = {Springer},
year = {2019},
location = {Porto, Portugal},
pages={256--272},
numpages={17},
doi={10.1007/978-3-030-32079-9_15},
isbn={978-3-030-32079-9},
abstract = {
In Runtime Verification (RV), monitoring a program means checking an
execution trace of the program for satisfactions and violations of
properties. The question of which properties can be effectively
monitored over ideal channels has mostly been answered by prior
work. However, program monitoring is often deployed for remote
systems where communications may be unreliable.
In this work, we address the question of what properties are
monitorable over an unreliable communication channel. We describe
the different types of mutations that may be introduced to an
execution trace and examine their effects 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 $\omega$-regular properties as monitorable
over channels with that mutation.
},
keywords={Monitorability, Unreliable channels, Automata theory}
}
@inproceedings{kauffman2019event,
author = {Kauffman, Sean and Fischmeister, Sebastian},
title = {Event Stream Abstraction Using Nfer: Demo Abstract},
booktitle = {International Conference on Cyber-Physical Systems (ICCPS'19)},
year = {2019},
isbn = {978-1-4503-6285-6},
location = {Montreal, Canada},
pages = {332--333},
numpages = {2},
doi = {10.1145/3302509.3313327},
publisher = {ACM Press},
abstract = {
We propose to demonstrate the open source implementation of
nfer (http://nfer.io), a language and system for abstracting
event streams. The tool is applicable to a wide variety of
cyber-physical systems, and supports both manual and mined
specifications. In addition to basic operation, we will
demonstrate standalone monitor generation and integration with
the popular R and Python languages. The demonstration will use
real-world data captured from applications such as an autonomous
vehicle and a hexacopter.
},
keywords = {Event stream processing, Runtime verification,
Telemetry comprehension, Temporal logic}
}
@article{kauffman2017inferring,
author = {Kauffman, Sean and Havelund, Klaus and
Joshi, Rajeev and Fischmeister, Sebastian},
title = {Inferring Event Stream Abstractions},
journal = {Formal Methods in System Design},
year = {2018},
volume = {53},
pages = {54--82},
numpages = {29},
doi = {10.1007/s10703-018-0317-z},
issn = {1572-8102},
abstract = {
We propose a formalism for specifying event stream
abstractions for use in spacecraft telemetry processing. Our
work is motivated by the need to quickly process streams with
millions of events generated by the Curiosity rover on Mars.
The approach builds a hierarchy of event abstractions for
telemetry visualization and querying to aid human comprehension.
Such abstractions can also be used as input to other runtime
verification tools. Our notation is inspired by Allen's Temporal
Logic, and provides a rule-based declarative way to express event
abstractions. We present an algorithm for applying specifications
to an event stream and explore modifications to improve the
algorithm's asymptotic complexity. The system is implemented in
both Scala and C, with the specification language implemented as
internal as well as external DSLs. We illustrate the solution
with several examples, a performance evaluation, and a real
telemetry analysis scenario.
}
}
@inproceedings{kauffman2017mining,
title = {Mining Temporal Intervals from Real-time System Traces},
author = {Kauffman, Sean and Fischmeister, Sebastian},
booktitle = {International Workshop on Software Mining (SoftwareMining'17)},
year = {2017},
doi = {10.1109/SOFTWAREMINING.2017.8100847},
pages = {1--8},
publisher = {IEEE},
isbn = {978-1-5386-1389-4},
location = {Urbana, USA},
abstract = {
We introduce a novel algorithm for mining temporal
intervals from real-time system traces with linear complexity
using passive, black-box learning. Our interest is in mining nfer
specifications from spacecraft telemetry to improve human and
machine comprehension. Nfer is a recently proposed formalism
for inferring event stream abstractions with a rule notation
based on Allen Logic. The problem of mining Allen's relations
from a multivariate interval series is well studied, but little
attention has been paid to generating such a series from symbolic
time sequences such as system traces. We propose a method to
automatically generate an interval series from real-time system
traces so that they may be used as inputs to existing algorithms
to mine nfer rules. Our algorithm has linear runtime and
constant space complexity in the length of the trace and can
mine infrequent intervals of arbitrary length from incomplete
traces. The paper includes results from case studies using logs
from the Curiosity rover on Mars and two other realistic datasets.
},
keywords={Complexity theory, Data mining;Measurement,
Real-time systems, Software, Telemetry, Tools}
}
@inproceedings{narayan2017system,
title = {System Call Logs with Natural Random Faults:
Experimental Design and Application},
author = {Narayan, Apurva and
Kauffman, Sean and
Morgan, Jack and
Tchamgoue, Guy Martin and
Joshi, Yogi and
Hobbs, Chris and
Fischmeister, Sebastian},
booktitle = {IEEE Workshop on Silicon Errors in
Logic -- System Effects (SELSE'17)},
year = {2017},
location = {Boston, USA},
publisher = {IEEE},
abstract = {
In this paper we present a large dataset for use in embedded
systems research which has been gathered from a realistic
development environment operating in the path of an accelerated
neutron beam. The dataset contains traces with events from a
real-time operating system as well as user events from a safety
critical application. All data is carefully timestamped and in
human understandable form. We present two use cases for this
dataset: mining timed regular expressions to extract system
specifications from clean and possibly anomalous data generated
during the operation of the neutron beam, and runtime monitoring
to extract information from traces with incomplete information.
The dataset is available for research at:
\url{http://doi.org/10.5281/zenodo.248008}
}
}
@inproceedings{kauffman2016nfer,
title = {nfer--A Notation and System for Inferring Event Stream
Abstractions},
author = {Kauffman, Sean and Havelund, Klaus and Joshi, Rajeev},
booktitle = {International Conference on Runtime Verification (RV'16)},
series = {LNCS},
volume = {10012},
pages = {235--250},
numpages = {16},
year = {2016},
doi = {10.1007/978-3-319-46982-9_15},
publisher = {Springer},
location = {Madrid, Spain},
abstract = {
We propose a notation for specifying event stream abstractions
for use in spacecraft telemetry processing. Our work is motivated
by the need to quickly process streams with millions of events
generated by the Curiosity rover on Mars. The approach builds a
hierarchy of event abstractions for telemetry visualization and
querying to aid human comprehension. Such abstractions can also
be used as input to other runtime verification tools. Our
notation is inspired by Allen's Temporal Logic, and provides a
rule-based declarative way to express event abstractions. The
system is written in Scala, with the specification language
implemented as an internal DSL. It is based on parallel executing
actors communicating via a publish-subscribe model. We
illustrate the solution with several examples, including a real
telemetry analysis scenario.
}
}
@inproceedings{kauffman2016towards,
title = {Towards a logic for inferring properties of event streams},
author = {Kauffman, Sean and Joshi, Rajeev and Havelund, Klaus},
booktitle = {International Symposium on Leveraging Applications
of Formal Methods (ISoLA'16)},
series = {LNCS},
volume = {9953},
pages = {394--399},
numpages = {6},
year = {2016},
doi = {10.1007/978-3-319-47169-3_31},
publisher = {Springer},
location = {Corfu, Greece},
abstract = {
We outline the background, motivation, and requirements of an
approach to create abstractions of event streams, which are
time-tagged sequences of events generated by an executing
software system. Our work is motivated by the need to process
event streams with millions of events that are generated by a
spacecraft, that must be processed quickly after they are
received on the ground. Our approach involves building a tool
that adds hierarchical labels to a received event stream. The
labels add contextual information to the event stream, and thus
make it easier to build tools for visualizing and analyzing
telemetry. We describe a notation for writing hierarchical
labeling rules; the notation is based on a modification of
Allen Temporal Logic, augmented with rule-definitions and
features for referring to data in data parameterized events.
We illustrate our notation and its use with an example.
}
}
@inproceedings{kauffman2016static,
title = {Static Transformation of Power Consumption for
Software Attestation},
author = {Kauffman, Sean and Moreno, Carlos and
Fischmeister, Sebastian},
booktitle = {International Conference on Embedded and
Real-Time Computing Systems and Applications (RTCSA'16)},
pages = {188--194},
numpages = {7},
year = {2016},
doi = {10.1109/RTCSA.2016.45},
publisher = {IEEE},
location = {Daegu, South Korea},
isbn = {978-1-5090-2479-7},
issn = {2325-1301},
abstract = {
Software attestation seeks to verify the authenticity of a
system without the aid of trusted hardware, and has important
applications in the field of security. Such attestation schemes
are of particular interest in the embedded domain, where
simplicity and limited resources constrain more complex security
solutions. At the same time, these properties enable attestation
approaches that rely on predictable side-effects. Most software
attestation schemes aim to verify the integrity of memory using
a combination of cryptographic schemes, internal side-effects
like TLB misses, and known timing constraints. However, little
attention has been paid to leveraging non-traditional
side-effects, in particular, externally observable side-effects
such as power consumption.
In this paper we introduce a method for software attestation
using power consumption as the side-effect. We show how to
circumvent the undecidable nature of program execution for this
purpose and present a static compiler transformation which
implements the technique. Our approach is less intrusive than
traditional software attestation because the system does not
require interruption to compute a cryptographic checksum. It is
particularly well suited to real-time systems where consistent
timing is more important than speed.
}
}
@inproceedings{moreno2016efficient,
title = {Efficient Program Tracing and Monitoring Through Power
Consumption -- With a Little Help From the Compiler},
author = {Moreno, Carlos and Kauffman, Sean and
Fischmeister, Sebastian},
booktitle = {Design, Automation \& Test in Europe Conference
\& Exhibition (DATE'16)},
pages = {1556--1561},
numpages = {6},
year = {2016},
doi = {10.3850/9783981537079_0829},
publisher = {IEEE},
location = {Dresden, Germany},
isbn = {978-3-9815-3707-9},
issn = {1558-1101},
abstract = {
Ensuring correctness and enforcing security are growing
concerns given the complexity of modern connected devices and
safety-critical systems. A promising approach is non-intrusive
runtime monitoring through reconstruction of program execution
traces from power consumption measurements. This can be used
for verification, validation, debugging, and security purposes.
In this paper, we propose a framework for increasing the
effectiveness of power-based program tracing techniques. These
systems determine the most likely block of source code that
produced an observed power trace (CPU power consumption as a
function of time). Our framework maximizes distinguishability
between power traces for different code blocks. To this end,
we provide a special compiler optimization stage that reorders
intermediate representation (IR) and determines the reorderings
that lead to power traces with highest distances between each
other, thus reducing the probability of misclassification. Our
work includes an experimental evaluation, using LLVM for an
ARM architecture. Experimental results confirm the effectiveness
of our technique.
}
}