Industrial Control Systems (ICS) are often built from geographically distributed components and often use programmable logic controllers for localized processes. Since verification of such systems is challenging because of both time sensitivity of the system specifications and the inherent asynchrony in distributed components, developing runtime assurance that verifies not just the correctness of different components, but also generates aggregated statistics of the systems is of interest. In this paper, we first present a general technique for runtime monitoring of distributed applications whose behavior can be modeled as input/output {\em streams} with an internal computation module in the partially synchronous semantics, where an imperfect clock synchronization algorithm is assumed. Second, we propose a generalized stream-based decentralized runtime verification technique. We also rigorously evaluate our algorithm on extensive synthetic experiments and several ICS and aircraft SBS message datasets.

翻译：工业控制系统通常由地理上分布的组件构成，并常采用可编程逻辑控制器执行本地化流程。由于系统规范的时间敏感性以及分布式组件固有的异步性，对此类系统的验证极具挑战性。因此，开发不仅验证各组件正确性、还能生成系统聚合统计信息的运行时保障技术具有重要意义。本文首先提出一种分布式应用运行时监测的通用技术，该技术将行为建模为具有内部计算模块的输入/输出流，采用部分同步语义，并假设存在非精确时钟同步算法。其次，我们提出一种基于流的通用去中心化运行时验证技术。最后，通过在大量合成实验以及多个工业控制系统与飞机SBS消息数据集上的严格评估，验证了所提算法的有效性。