  


Formal property verification in a conformance testing framework
Houssam Abbas (hyabbasasu.edu) Abstract: In modelbased design of cyberphysical systems, such as switched mixedsignal circuits or softwarecontrolled 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 rewriting 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 Citation: Download: [PDF] Entry Submitted: 07/25/2014 Modify/Update this entry  
Visitors  Authors  More about us  Links  
Subscribe, Unsubscribe Digest Archive Search, Browse the Repository

Submit Update Policies 
Coordinator's Board Classification Scheme Credits Give us feedback 
Optimization Journals, Sites, Societies  