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$的设计和执行,并介绍了其功能和模块。为了提高工具对非专家用户的可用性,我们还提供了一份量化属性模板清单。