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 (Print)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

Other

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

Fingerprint

Conformance Testing
Testing
Model
Quantify
Automatic Code Generation
Model-based Design
Embedded Processor
Simulink
Distance Measure
Rewriting
Temporal logic
Soundness
Temporal Logic
Framework
Computational Methods
Fidelity
Simplification
Computational methods
Specification
Metric

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] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/MEMCOD.2014.6961854

Formal property verification in a conformance testing framework. / Abbas, Houssam; Mittelmann, Hans; Fainekos, Georgios.

12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014. Institute of Electrical and Electronics Engineers Inc., 2014. p. 155-164 6961854.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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., 6961854, Institute of Electrical and Electronics Engineers Inc., pp. 155-164, 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014, Lausanne, Switzerland, 10/19/14. https://doi.org/10.1109/MEMCOD.2014.6961854
Abbas H, Mittelmann H, Fainekos G. Formal property verification in a conformance testing framework. In 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014. Institute of Electrical and Electronics Engineers Inc. 2014. p. 155-164. 6961854 https://doi.org/10.1109/MEMCOD.2014.6961854
Abbas, Houssam ; Mittelmann, Hans ; Fainekos, Georgios. / Formal property verification in a conformance testing framework. 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 155-164
@inproceedings{bac712193368427e9a4701d557bb1c29,
title = "Formal property verification in a conformance testing framework",
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.",
author = "Houssam Abbas and Hans Mittelmann and Georgios Fainekos",
year = "2014",
month = "11",
day = "18",
doi = "10.1109/MEMCOD.2014.6961854",
language = "English (US)",
isbn = "9781479953387",
pages = "155--164",
booktitle = "12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Formal property verification in a conformance testing framework

AU - Abbas, Houssam

AU - Mittelmann, Hans

AU - Fainekos, Georgios

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

SN - 9781479953387

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.

ER -