From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires to reason about complex spatio-temporal properties of physical and/or computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and to reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing their spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.


翻译:从生物系统到网络物理系统,监测这些动态系统的行为往往需要了解动态相互联系并在特定空间配置中安排的物理和(或)计算实体的复杂时空特性。Spatio-Temoal Areating and Escape Locic(STREL)是最近一种基于逻辑的正式语言,旨在说明和解释spatio-时间特性。STREL认为每个系统实体是代表其空间安排的动态加权图表的节点。每个节点产生一组混合分析信号,描述显示显示该节点行为在计算和物理数量方面的演变过程。虽然有非在线算法可用于监测STREL对登录模拟痕迹的规格,但在这里我们首次调查一种在线算法,使系统执行或模拟期间的运行时间核查能够进行。我们的方法通过考虑不精确的信号和增强逻辑的语义来扩展最初的框架,从而有可能表达系统行为是否符合其规格的部分保证。最后,我们在现实世界环境监测案例研究中展示了我们的方法。

0
下载
关闭预览

相关内容

【经典书】贝叶斯编程,378页pdf,Bayesian Programming
专知会员服务
247+阅读 · 2020年5月18日
简明扼要!Python教程手册,206页pdf
专知会员服务
47+阅读 · 2020年3月24日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
【新书】Python编程基础,669页pdf
专知会员服务
194+阅读 · 2019年10月10日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
机器人开发库软件大列表
专知
10+阅读 · 2018年3月18日
已删除
将门创投
7+阅读 · 2017年7月11日
Arxiv
0+阅读 · 2021年11月8日
Arxiv
0+阅读 · 2021年11月4日
Online Estimation for Functional Data
Arxiv
0+阅读 · 2021年11月4日
VIP会员
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
机器人开发库软件大列表
专知
10+阅读 · 2018年3月18日
已删除
将门创投
7+阅读 · 2017年7月11日
Top
微信扫码咨询专知VIP会员