Affordable Access

Quantitative Corner Case Feature Analysis of Hybrid Automata with ForFET-SMT

Authors
  • Anastasio Bruto Da Costa, Antonio
  • Dasgupta, Pallab
  • Kekatos, Nikolaos
Publication Date
Dec 31, 2020
Source
HAL
Keywords
Language
English
License
Unknown
External links

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-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.

Report this publication

Statistics

Seen <100 times