### 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 language | English (US) |
---|---|

Title of host publication | 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 |

Publisher | Institute of Electrical and Electronics Engineers Inc. |

Pages | 155-164 |

Number of pages | 10 |

ISBN (Print) | 9781479953387 |

DOIs | |

State | Published - Nov 18 2014 |

Event | 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 - Lausanne, Switzerland Duration: Oct 19 2014 → Oct 21 2014 |

### Other

Other | 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 |
---|---|

Country | Switzerland |

City | Lausanne |

Period | 10/19/14 → 10/21/14 |

### Fingerprint

### ASJC Scopus subject areas

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

### Cite this

*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.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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

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 -