TY - GEN
T1 - Formal feature analysis of hybrid automata
AU - Da Costa, Antonio Anastasio Bruto
AU - Dasgupta, Pallab
AU - Frehse, Goran
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/12/27
Y1 - 2016/12/27
N2 - Circuits and systems that have to deal with real valued artifacts often need to be evaluated not only for correct behaviors, but also the margins by which they satisfy the design intent. Our definition of 'features' formally extends the classical notion of 'assertions' by overlaying constructs for specifying real valued functions over matches of assertions, thereby providing a powerful language framework for specifying real valued properties of the system. In this paper we present, for the first time, methods for formal evaluation of feature ranges on hybrid automata models which are extensively used for modeling switched control systems. We demonstrate the methodology over three case studies, namely a cruise control system, a DC-DC Buck Regulator and a Li-ion battery charger.
AB - Circuits and systems that have to deal with real valued artifacts often need to be evaluated not only for correct behaviors, but also the margins by which they satisfy the design intent. Our definition of 'features' formally extends the classical notion of 'assertions' by overlaying constructs for specifying real valued functions over matches of assertions, thereby providing a powerful language framework for specifying real valued properties of the system. In this paper we present, for the first time, methods for formal evaluation of feature ranges on hybrid automata models which are extensively used for modeling switched control systems. We demonstrate the methodology over three case studies, namely a cruise control system, a DC-DC Buck Regulator and a Li-ion battery charger.
U2 - 10.1109/MEMCOD.2016.7797740
DO - 10.1109/MEMCOD.2016.7797740
M3 - Conference contribution
AN - SCOPUS:85010800043
T3 - 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
SP - 2
EP - 11
BT - 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
Y2 - 18 November 2016 through 20 November 2016
ER -