  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.
