Worst-Case Execution Time Calculation for Query-Based Monitors by Witness Generation

TL;DR

This paper introduces a semantic-aware static analysis method to accurately estimate the worst-case execution time of graph-query-based runtime monitors in cyber-physical systems, enhancing safety guarantees in real-time applications.

Contribution

It presents a novel WCET estimation technique that leverages domain-specific information and witness generation to produce tight, safe execution time bounds for data-driven monitoring programs.

Findings

Generated witness models reveal worst-case execution scenarios.

The approach produces tighter WCET bounds than existing static analyzers.

Experimental results validate the method's effectiveness on real-time platforms.

Abstract

Runtime monitoring plays a key role in the assurance of modern intelligent cyber-physical systems, which are frequently data-intensive and safety-critical. While graph queries can serve as an expressive yet formally precise specification language to capture the safety properties of interest, there are no timeliness guarantees for such auto-generated runtime monitoring programs, which prevents their use in a real-time setting. While worst-case execution time (WCET) bounds derived by existing static WCET estimation techniques are safe, they may not be tight as they are unable to exploit domain-specific (semantic) information about the input models. This paper presents a semantic-aware WCET analysis method for data-driven monitoring programs derived from graph queries. The method incorporates results obtained from low-level timing analysis into the objective function of a modern graph solver. This allows the systematic generation of input graph models up to a specified size (referred to as witness models) for which the monitor is expected to take the most time to complete. Hence the estimated execution time of the monitors on these graphs can be considered as safe and tight WCET. Additionally, we perform a set of experiments with query-based programs running on a real-time platform over a set of generated models to investigate the relationship between execution times and their estimates, and compare WCET estimates produced by our approach with results from two well-known timing analyzers, aiT and OTAWA.