Bibtex Entries

@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},
  origin = {Postdoc},
  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.
  }
}