Conformance Relations and Hyperproperties for Doping Detection in Time and Space

TL;DR

This paper introduces a new formal framework for doping detection in cyber-physical systems by defining conformance relations and hyperproperties, supported by a novel temporal logic extension, demonstrated through a diesel emission case study.

Contribution

It proposes a generalized notion of doping cleanness using conformance relations and hyperproperties, and develops HyperSTL* for monitoring these properties in cyber-physical systems.

Findings

Effective doping detection in a diesel emission case study

Formalization of conformance-based cleanness in cyber-physical systems

Introduction of HyperSTL* logic for hyperproperty specification

Abstract

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.