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. The main challenge is that the worst-case execution time (WCET) bounds provided by current static WCET computation methods for such programs can only provide very conservative and impractical estimations, which would result in wasteful resource allocation or inadequate scheduling of monitors. This paper presents a 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 WCET. Moreover, in case the runtime graph model outgrows the size that was used to determine WCET at design time, our approach provides a fast but more conservative recomputation of safe execution time bounds on-the-fly using runtime model statistics. The benefit is that such on-line WCET estimation is still comparable to the one which solely relies on traditional approaches. Finally, we perform experiments with query-based programs executed in a real-time platform over a set of generated models to investigate the relationship between execution times and their estimates, and we compare WCETs obtained with the different approaches.
翻译:运行时间监测在确保现代智能网络物理系统方面发挥着关键作用,这些系统往往是数据密集和安全临界的。虽然图表查询可以作为一种表达式但正式精确的规格语言,用来记录感兴趣的安全性能,但这种自动生成运行时间监测程序没有及时的保证,从而无法在实时环境下使用。主要挑战是,目前静态的WCET计算方法提供的最坏执行时间(WCET),只能提供非常保守和不切实际的估计,从而导致资源浪费性资源分配或监测器的时间安排不足。本文为图表查询产生的数据驱动的监测程序提供了一种计算方法。该方法将低级别时间分析的结果纳入现代图形求解器的客观功能中,从而使得无法在实时监测中系统地生成一定规模的输入图表模型模型模型模型(称为证人模型),预计要用最长时间来完成。因此,这些图表上监测器的估计执行时间将被视为安全的WCET。此外,在运行的运行时间图中,我们使用一个运行的离线模型,但在使用一个可比较的时间比的运行时间规则,从而确定我们使用快速执行时间规则的计算方法。