Formal Feature Interpretation of Hybrid Systems

TL;DR

This paper introduces a method for formally interpreting features in hybrid automata, enabling quantitative behavioral analysis and extraction of corner case traces using SMT solvers, demonstrated on control and circuit examples.

Contribution

It presents an improved feature interpretation method for hybrid automata and utilizes SMT solvers to extract specific behavioral traces, advancing formal analysis techniques.

Findings

Effective feature interpretation over hybrid automata

Use of SMT solvers to find corner case traces

Demonstrated on control and circuit domain examples

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.