The analysis and verification of hybrid automata (HA) models against rich formal properties can be a challenging task. Existing methods and tools can mainly reason whether a given property is satisfied or violated. However, such qualitative answers might not provide sufficient information about the model behaviors. This paper presents the ForFET$^{SMT}$ tool which can be used to reason quantitatively about such properties. It employs feature automata and can evaluate quantitative property corners of HA. ForFET$^{SMT}$ uses two third-party formal verification tools as its backbone: the SpaceEx reachability tool and the SMT solver dReach/dReal. Herein, we describe the design and implementation of ForFET$^{SMT}$ and present its functionalities and modules. To improve the usability of the tool for non-expert users, we also provide a list of quantitative property templates.


翻译:现有方法和工具主要可以说明某一财产是否满足或被违反,然而,这类定性答案可能无法提供关于模型行为的充分信息。本文件介绍了可用来定量解释这些特性的FET$ ⁇ SMT}$工具。它使用自动模型特性,并可以评估HA的量化属性角。FET$ ⁇ SMT}$使用两个第三方正式核查工具作为其主干线:SpaceEx可达性工具和SMT Ssuplugr dReach/dReal。我们描述了FET$ ⁇ SMT$的设计和执行,并介绍了其功能和模块。为了提高工具对非专家用户的可用性,我们还提供了一份量化属性模板清单。

0
下载
关闭预览

相关内容

最新《Transformers模型》教程,64页ppt
专知会员服务
306+阅读 · 2020年11月26日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
商业数据分析,39页ppt
专知会员服务
160+阅读 · 2020年6月2日
一份循环神经网络RNNs简明教程,37页ppt
专知会员服务
172+阅读 · 2020年5月6日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
LibRec 精选:AutoML for Contextual Bandits
LibRec智能推荐
7+阅读 · 2019年9月19日
CVPR2019教程《胶囊网络(Capsule Networks)综述》,附93页PPT
GAN生成式对抗网络
29+阅读 · 2019年6月21日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
SIGIR2019 接收论文列表
专知
18+阅读 · 2019年4月20日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
神器Cobalt Strike3.13破解版
黑白之道
12+阅读 · 2019年3月1日
ACL 2018 计算语言学协会接受论文列表
专知
3+阅读 · 2018年4月27日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
A Spectral Approach to Polytope Diameter
Arxiv
0+阅读 · 2021年3月3日
VIP会员
Top
微信扫码咨询专知VIP会员