Quantitative Corner Case Feature Analysis of Hybrid Automata with ForFET$^{SMT}$
Abstract
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 tool which can be used to reason quantitatively about such properties. It employs feature automata and can evaluate quantitative property corners of HA. ForFET 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 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.
Keywords
Cite
@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}
}