Formal Feature Interpretation of Hybrid Systems
Logic in Computer Science
2019-02-25 v2 Software Engineering
Abstract
In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.
Keywords
Cite
@article{arxiv.1711.00669,
title = {Formal Feature Interpretation of Hybrid Systems},
author = {Antonio Anastasio Bruto da Costa and Goran Frehse and Pallab Dasgupta},
journal= {arXiv preprint arXiv:1711.00669},
year = {2019}
}