This website requires JavaScript.
DOI: 10.4204/EPTCS.395.14

Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers

C\'eline Bellanger (ENACUniversit\'e de Toulouse)Pierre-Lo\"ic Garoche (ENAC ...+3 Universit\'e de Toulouse)
Nov 2023
0被引用
0笔记
摘要原文
Signal Temporal Logic (STL) is a convenient formalism to express bounded horizon properties of autonomous critical systems. STL extends LTL to real-valued signals and associates a non-singleton bound interval to each temporal operators. In this work we provide a rigorous encoding of non-nested discrete-time STL formulas into Lustre synchronous observers. Our encoding provides a three-valued online semantics for the observers and therefore enables both the verification of the property and the search of counter-examples. A key contribution of this work is an instrumented proof of the validity of the implementation. Each node is proved correct with respect to the original STL semantics. All the experiments are automated with the Kind2 model-checker and the Z3 SMT solver.
展开全部
机器翻译
AI理解论文&经典十问
图表提取
参考文献
发布时间 · 被引用数 · 默认排序
被引用
发布时间 · 被引用数 · 默认排序
社区问答