重新探讨用于使用STL对Lustre进行运行时验证的同步观察器
Synchronous Observers Revisited for Runtime Verification of Lustre Using STL
浏览论文内容
中文总结 AI 辅助
本文提出将SSTL编译为Lustre同步观察器的技术，支持有界SSTL属性嵌套与全局无界外层运算符，开发了可视化工具并通过两个案例验证了方法的有效性。
中文摘要 AI 辅助
信号时态逻辑（Signal Temporal Logic，STL）是一种流行的形式化方法，用于描述网络物理系统的时态安全属性，最常用于运行时验证。在同步语言家族中，安全属性则被表示为同步观察器，这些模块可与程序组合以进行静态验证，同时也是适用于运行时验证的可执行规范，不过这种用法很少被探讨。我们提出了一种技术，将STL的同步片段（Synchronous STL，SSTL）编译为数据流语言Lustre中的同步观察器。与以往工作不同，我们通过模块化编译支持有界SSTL属性的任意嵌套，并允许全局无界的外层运算符用于在线监控；生成的观察器既用于运行时验证，又可作为附带产物用于Kind2模型检查器的静态验证。我们还开发了一个交互式可视化工具，可在可编辑的轨迹上渲染属性的三值判决，并通过两个文献中的案例研究进行评估：一个弹簧质量系统和一个跟车巡航控制器。
英文摘要
Signal Temporal Logic (STL) is a popular formalism for the temporal safety properties of cyber-physical systems, most often used for runtime verification. In the synchronous family of languages, safety properties are instead expressed as synchronous observers, modules composed with a program for static verification, which are also runnable specifications suitable for runtime verification, though this use is rarely explored. We present a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre. Unlike previous work, we allow arbitrary nesting of bounded SSTL properties via modular compilation, and admit a globally unbounded outer operator for online monitoring; the resulting observers serve both runtime verification and, as a by-product, static verification with the Kind2 model checker. We further contribute an interactive visualiser that renders a property's three-valued verdict over an editable trace, and evaluate on two case studies from the literature: a spring-mass system and a car-following cruise controller.
