Optimization Online


Formal property verification in a conformance testing framework

Houssam Abbas (hyabbas***at***asu.edu)
Hans Mittelmann (mittelmann***at***asu.edu)
Georgios Fainekos (fainekos***at***asu.edu)

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 (implementation). 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, and demonstrate their use on several examples. 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 these rules via experiments.

Keywords: dynamical systems, system models, conformance

Category 1: Applications -- Science and Engineering


Download: [PDF]

Entry Submitted: 07/25/2014
Entry Accepted: 07/25/2014
Entry Last Modified: 01/08/2015

Modify/Update this entry

  Visitors Authors More about us Links
  Subscribe, Unsubscribe
Digest Archive
Search, Browse the Repository


Coordinator's Board
Classification Scheme
Give us feedback
Optimization Journals, Sites, Societies
Mathematical Optimization Society