Abstract

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.

Original languageEnglish (US)
Title of host publication12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages155-164
Number of pages10
ISBN (Electronic)9781479953387
DOIs
StatePublished - Nov 18 2014
Event12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 - Lausanne, Switzerland
Duration: Oct 19 2014Oct 21 2014

Publication series

Name12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014

Other

Other12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014
CountrySwitzerland
CityLausanne
Period10/19/1410/21/14

    Fingerprint

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Hardware and Architecture
  • Software
  • Modeling and Simulation

Cite this

Abbas, H., Mittelmann, H., & Fainekos, G. (2014). Formal property verification in a conformance testing framework. In 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 (pp. 155-164). [6961854] (12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/MEMCOD.2014.6961854