Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding vacuity in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying the given constraints is a key enabler for the viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution, and can be very inefficient to produce legal scenarios of interest. We show how, given a set of constraints on the input scenarios succinctly defined by finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification.


翻译:以模型为基础的方法来核查非结束性网络-物理系统(CPS),这种方法通常依赖在可能不同期限的输入假设情景下对核查系统(SUV)模型进行数字模拟,这种模拟可能是在满足特定限制的情况下选择的,这些限制通常来自对SUV投入及其业务环境的要求(或假设),以及执行其他条件,目的是,例如,通过以模拟为基础的统计模式检查,优先考虑(通常非常长的)核查活动,例如,通过明确采用某些要求的假设情景,或避免其满意度的出现。在这一背景下,有可能在随机(已知的随机分布,例如统一)内部或高效率地(以统一的随机顺序)抽样抽取“核查系统”模型模型模型模型模型模型模型模型模型模型模型模型模型模型,例如明确使用某些限制,或避免其满意度出现空洞。

0
下载
关闭预览

相关内容

专知会员服务
41+阅读 · 2021年4月2日
专知会员服务
25+阅读 · 2021年4月2日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
鲁棒机器学习相关文献集
专知
8+阅读 · 2019年8月18日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
人工智能 | COLT 2019等国际会议信息9条
Call4Papers
6+阅读 · 2018年9月21日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
人工智能 | 国际会议截稿信息9条
Call4Papers
4+阅读 · 2018年3月13日
计算机类 | 国际会议信息7条
Call4Papers
3+阅读 · 2017年11月17日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Arxiv
0+阅读 · 2021年10月28日
VIP会员
相关VIP内容
专知会员服务
41+阅读 · 2021年4月2日
专知会员服务
25+阅读 · 2021年4月2日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
鲁棒机器学习相关文献集
专知
8+阅读 · 2019年8月18日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
人工智能 | COLT 2019等国际会议信息9条
Call4Papers
6+阅读 · 2018年9月21日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
人工智能 | 国际会议截稿信息9条
Call4Papers
4+阅读 · 2018年3月13日
计算机类 | 国际会议信息7条
Call4Papers
3+阅读 · 2017年11月17日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Top
微信扫码咨询专知VIP会员