Understanding the Timed Distributed Trace of a Partially Synchronous System at Runtime

TL;DR

This paper introduces PARO, a framework for analyzing timed distributed traces in cyber-physical systems with imperfect clocks, using partial synchrony models, timed automata, and 3-valued semantics to verify real-time properties at runtime.

Contribution

It proposes a novel runtime verification framework combining partial synchrony, timed automata, and 3-valued semantics, enabling effective analysis of real-time properties in cyber-physical systems.

Findings

PARO effectively models system traces using timed automata.

The framework supports real-time property verification with 3-valued semantics.

Performance measurements demonstrate cost-effectiveness across various settings.

Abstract

It has gained broad attention to understand the timed distributed trace of a cyber-physical system at runtime, which is often achieved by verifying properties over the observed trace of system execution. However, this verification is facing severe challenges. First, in realistic settings, the computing entities only have imperfectly synchronized clocks. A proper timing model is essential to the interpretation of the trace of system execution. Second, the specification should be able to express properties with real-time constraints despite the asynchrony, and the semantics should be interpreted over the currently-observed and continuously-growing trace. To address these challenges, we propose PARO - the partially synchronous system observation framework, which i) adopts the partially synchronous model of time, and introduces the lattice and the timed automata theories to model the trace of system execution; ii) adopts a tailored subset of TCTL to specify temporal properties, and defines the 3-valued semantics to interpret the properties over the currently-observed finite trace; iii) constructs the timed automaton corresponding to the trace at runtime, and reduces the satisfaction of the 3-valued semantics over finite traces to that of the classical boolean semantics over infinite traces. PARO is implemented over MIPA - the open-source middleware we developed. Performance measurements show the cost-effectiveness of PARO in different settings of key environmental factors.