Evidence-Oriented Tracing and Verification, The Declaration of Timeprints

Abstract

With the unprecedented jump in reliance on digital systems, the expectations about their reliability, safety and correctness rise as well. The complexity of these systems is increasing, while the means for ensuring and checking systems correctness and safety are lagging behind. The analysis and inspection of potential root-causes (behind such failures) focus on finding bugs, noncompliance or shortage within the design and/or process artifacts, beside the direct traces obtained from in-field execution. Although obtaining accurate and independent traces of the system's in-field operation would be very useful; it is not usually pursued, because of the prohibitive resultant amounts of data.

From user’s perspective, continuously logged digital-execution traces are needed as evidence of in-field execution. These traces need to be independent (not just self reporting), accurate (not coarse, and triggered automatically by the physical execution taking place), and affordable (light: so that they can be efficiently logged, stored and processed). To reach this, the thesis proposes periodically logging a light-weight temporal trace-print from physical signal execution, which we call the Timeprints-trace. Such trace is meant to act as a signature of the period of execution it summarizes. From these signatures, some details can be checked and properties about them can be formally verified. We call this form of verification: "Evidence-Oriented", in which we formally check offline (and on-demand), and prove properties of what happened. The Timeprints open the door for a wide range of deployment-phase accurate timing-properties verification; some of which are also shown in the thesis.