TY - GEN
T1 - Formal property verification in a conformance testing framework
AU - Abbas, Houssam
AU - Mittelmann, Hans
AU - Fainekos, Georgios
N1 - Publisher Copyright:
© 2014 IEEE.
PY - 2014/11/18
Y1 - 2014/11/18
N2 - In model-based design of cyber-physical systems, such as switched mixed-signal circuits or software-controlled physical systems, it is common to develop a sequence of system models of different fidelity and complexity, each appropriate for a particular design or verification task. In such a sequence, one model is often derived from the other by a process of simplification or implementation. E.g. a Simulink model might be implemented on an embedded processor via automatic code generation. Three questions naturally present themselves: how do we quantify closeness between the two systems? How can we measure such closeness? If the original system satisfies some formal property, can we automatically infer what properties are then satisfied by the derived model? This paper addresses all three questions: we quantify the closeness between original and derived model via a distance measure between their outputs. We then propose two computational methods for approximating this closeness measure. Finally, we derive syntactical re-writing rules which, when applied to a Metric Temporal Logic specification satisfied by the original model, produce a formula satisfied by the derived model. We demonstrate the soundness of the theory with several experiments.
AB - In model-based design of cyber-physical systems, such as switched mixed-signal circuits or software-controlled physical systems, it is common to develop a sequence of system models of different fidelity and complexity, each appropriate for a particular design or verification task. In such a sequence, one model is often derived from the other by a process of simplification or implementation. E.g. a Simulink model might be implemented on an embedded processor via automatic code generation. Three questions naturally present themselves: how do we quantify closeness between the two systems? How can we measure such closeness? If the original system satisfies some formal property, can we automatically infer what properties are then satisfied by the derived model? This paper addresses all three questions: we quantify the closeness between original and derived model via a distance measure between their outputs. We then propose two computational methods for approximating this closeness measure. Finally, we derive syntactical re-writing rules which, when applied to a Metric Temporal Logic specification satisfied by the original model, produce a formula satisfied by the derived model. We demonstrate the soundness of the theory with several experiments.
UR - http://www.scopus.com/inward/record.url?scp=84916614011&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84916614011&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2014.6961854
DO - 10.1109/MEMCOD.2014.6961854
M3 - Conference contribution
AN - SCOPUS:84916614011
T3 - 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014
SP - 155
EP - 164
BT - 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014
Y2 - 19 October 2014 through 21 October 2014
ER -