Formal Analysis of Hybrid Systems Using Feature Indented Assertions
share
Model based design is a recommended step in the design of embedded control systems. A formal analysis of models helps in arriving at provably correct designs that meet the necessary functional requirements. Often such analysis needs to look beyond functional correctness to evaluate the margins of behavioral attributes. Our notion of features addresses this requirement. The syntactic fabric of our feature definitions enjoys similarity with assertion languages; however, unlike assertions, the consequent of features are real valued expressions representing the feature value. In this article, we give insights into the extensive work we have done in the formal analysis of features for hybrid models. We describe a methodology for abstract interpretation of features over hybrid automata models, leveraging reachability solvers for extracting feature ranges formally and further demonstrate how Satisfiability Modulo Theory (SMT) solvers can be used for extracting behavioural traces corresponding to corner cases of a feature.
READ FULL TEXT