Conformance Relations and Hyperproperties for Doping Detection in Time and Space — Case Study Details

The Jupyter notebook file and raw data is available here.

For our analysis, we use the Pandas data analysis and manipulation tool to represent and manipulate data. For visualisation, we show data graphically using the matplotlib library.

The results of our experiments are stored in individual CSV files. The raw data is loaded in variables with a leading underscore. For the main analysis part, we remove the data that was recordered before and after each test. A test starts at time point 0 and ends with time point 1179 (except for DoubleNEDC, which is twice as long). The trimmed data is stored in the appropriate variable without the leading underscore.

Experiments are represented by tables. Retimings are applied on two experiments, resulting in a merged single table. The following functions provide auxiliary tools to merge and separate (merged) tables.

Like all experiments, we executed NEDC twice. For simplicity, we compare all non-NEDC experiments only to one reference NEDC, which is the average of NEDC-1 and NEDC-2. Unfortunately, due to technical problems no OBD data (velocity, engine speed) is available for NEDC-1, so we take only data from NEDC-2. The averaged NEDC will be available as nedc in the following cells.

For the evaluation of our experiments, we accumulate NOx values over 1180 seconds. The accumulated value is given in milligrams per kilometre. Function integrateData computes the sum of the values in a column, w.r.t. a given step function. It can compute the sum of all NOx values (which are given in grams) and can compute the total distance that the test vehicle travelled during the test execution. For the computation of the total distance, the speed values must be converted from km/h to m/s, and the result from m in km. Function accumulatedNOxPerTotalDistance is doing these conversions and computations.

For later comparisons, we need accumulated NOx values and prepare the appropriate values here.

Another utility function we will need is getMaximumValueError, which, for a retiming given as a merged table, computes the row-wise maximum absolute difference of values in column key and the appropriate renamed column. It returns the largest of these differences.

In order to show test results graphically, we use function plotCycles to compare velocity and NOx values of two experiments. The blue and orange lines show speed and NOx values, respectively, for the first table. Green and red are used for the second. Time ticks, NOx ticks and time values can be modified if necessary.

For example, the following command plots a comparison of NEDC and PermNEDC-1 (with NOx given in g/s).

Retiming Experiments

In the following, we will investigate each of the three experiment types mentioned in the paper: NEDC permutations, lengthened test cycles and hybrid conformance.

All functions below assume that the data is sampled by 1Hz, which is asserted with the following function.

NEDC Permutations

The PermNEDC cycle is generated by splitting the UDC subcycle into seven pieces. The length of each piece is given by euc0 to euc6 below. The length of EUDC is given in extra. We encode the NEDC and PermNEDC in lists, that store sequences of index and length of UDC pieces. The original EUC is stored in ops (length of the pieces) and [0,1,2,3,4,5,6] (the index of the pieces). The four UDC repetitions are encoded by nedcOps and nedcOpsi. Permutation NEDC is defined by the permuted ops1234 and opsi1234 lists given below.

The functions nedc2perm and perm2nedc use this encoding to map a time point t of NEDC to the appropriate t' of PermNEDC (i.e., t has been shifted to the new position t'). Similarly, perm2nedc computes the inverse of nedc2perm.

The pair of retiming functions (nedc2perm, perm2nedc) represents the retiming $\mathsf{Ret}_p$. The functions doPermRetiming1 and doPermRetiming2 below, apply the retiming functions. Retiming functions are applied to two experiment tables and result in a single, merged, table. To show the result visually, splitExperiments is used to separate the original and retimed version of the original tables.

For example, doPermRetiming1(nedc, perm1) keeps nedc untouched, but reorders perm1, such that it looks like the NEDC. The result is shown in the first plot. doPermRetiming2(nedc, perm1) does the opposite. It leaves perm1 unchanged but reorders nedc to match the time structure of perm1. The result is shown in third and fourth plot.

The NOx value errors are as reported in the paper.

An alternative retiming presented in the paper was the anarchy retiming $\mathsf{Ret}_a$. The anarchy retiming allows any permutation of the NEDC. To compute one of the best retimings w.r.t. the maximum value error, we sort NEDC and PermNEDC by velocity and then merge the sorted tables. This is already a valid retiming, but it is more convenient to have it sorted by the Time column of either NEDC or PermNEDC. We chose NEDC in the function below.

The anarchy retiming can be applied in a similar way as the permutation retiming above. However, every retiming returned by doAnarchyRetiming encodes two retiming functions that are valid according to $\mathsf{Ret}_a$. The first by mapping Time to Time Ref and the second by taking the inverse mapping from Time Ref to Time. Intuitively, each of the retiming functions can be constructed by sorting the merged table by either Time or Time Ref. As the difference between the two functions is insignificant, we only consider the Time Ref to Time function.

A careful inspection of the plot below shows, that the blue and green line are fitting a little bit better to each other than in the previous plots.

As we report in the main paper, the maximum value error with the anarchy retiming is 3 km/h for both test cycles.

Double NEDC

The retiming functions for DoubleNEDC are simpler than those for PermNEDC, and implemented in nedc2double and double2nedc.

They can be applied as explained for Permutation NEDC above; the whole cell below is structurally equivalent to the one defining doPermRetiming1. Effectively, the main difference is, that doDoubleRetiming1 shortens DoubleNEDC by dropping its second half and doDoubleRetiming2 lengthens NEDC by appending a second copy of itself. Appropriately, the first two figures show a 1180 seconds long experiment, wereas the last two plots show data for 2360 (= 2 * 1180) seconds.

The maximum value error is as reported in the paper.

SineNEDC & Hybrid Conformance

The paper sketches an algorithm to compute the minimal value error $\epsilon$ such that hybrid conformance holds for a given $\tau$. The algorithm is implemented below.

As explained in the paper, hybrid conformance cannot be applied to PermNEDC and DoubleNEDC directly. For these cycles, hybrid retiming must be composed with their original retiming. We realise the composition explicitly by working with the already retimed versions of NEDC, PermNEDC and DoubleNEDC. The retimed versions are passed to globalMin as explained in the paper.

Finally, we will verify that Table 1 in our paper is correct. To this end, we compute the minimal epsilons for all experiments for every tau in tauOfInterest (which are exacly the taus from our paper).

computeFullTable assumes hybrid conformance functions, that only receive the time threshold $\tau$ and return the minimal value threshold $\epsilon$. For hybrid conformance (i.e., SineNEDC) we need an auxiliary function pHybridValueError, that generates these plain hybrid conformance functions. The hybrid conformance functions for PermNEDC and DoubleNEDC already satisfy this constraint. Each row of the table is computed by iteratively calling the hybrid conformance functions with the taus in tauOfInterest. computeFullTable transforms the computed rows into a table.