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.