基于 ForFET$^{SMT}$ 的混合自动机定量极端情形特征分析
形式语言与自动机理论
2021-01-06 v1 计算机科学中的逻辑
摘要
对混合自动机（HA）模型针对丰富形式化性质的分析与验证可能是一项具有挑战性的任务。现有方法与工具主要能推断给定性质是否被满足或违反。然而，此类定性回答可能无法提供关于模型行为的充分信息。本文介绍 ForFET 工具，可用于对此类性质进行定量推断。它采用特征自动机，并能评估 HA 的定量性质极端情形。ForFET 以两个第三方形式化验证工具为骨干：SpaceEx 可达性工具与 SMT 求解器 dReach/dReal。在此，我们描述 ForFET 的设计与实现，并展示其功能与模块。为提升该工具对非专业用户的可用性，我们还提供了一份定量性质模板列表。
引用
@article{arxiv.2101.01255,
title = {Quantitative Corner Case Feature Analysis of Hybrid Automata with ForFET$^{SMT}$},
author = {Antonio Anastasio Bruto da Costa and Pallab Dasgupta and Nikolaos Kekatos},
journal= {arXiv preprint arXiv:2101.01255},
year = {2021}
}