将 STL 算子作为同步观测器进行形式化规约与验证的探析
计算机科学中的逻辑
2023-11-17 v1
摘要
信号时序逻辑（STL）是一种表达自主关键系统有界时域性质的有效形式。STL 将 LTL 扩展至实值信号，并为每个时序算子关联一个非单点限界区间。在本文中，我们提供了将非嵌套离散时间 STL 公式严格编码为 Lustre 同步观测器的方法。我们的编码为观测器提供了三值在线语义，从而同时支持性质验证与反例搜索。本工作的一个关键贡献是对实现有效性的工具化证明。每个节点都针对原始 STL 语义被证明是正确的。所有实验均通过 Kind2 模型检测器与 Z3 SMT 求解器自动化完成。
引用
@article{arxiv.2311.09788,
title = {Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers},
author = {Céline Bellanger and Pierre-Loïc Garoche and Matthieu Martel and Célia Picard},
journal= {arXiv preprint arXiv:2311.09788},
year = {2023}
}
备注
In Proceedings FMAS 2023, arXiv:2311.08987