The standard refinement approach for verifying systems consists of constructing an abstract model of the system, proving properties on the abstract level, and finally showing that the real model is a refinement of the abstract model, i.e., every trace in the actual model is present in the abstract one. In many control systems applications, the ultimate objective is to show that the system stays within some parameters. A slight deviation from the ideal behavior may be acceptable provided some constraints are not violated. We are working on a notion of refinement which considers metrics between traces. The standard refinement relation looks at the Boolean metric on traces--either the two traces are the same, or they are not. Approximate refinement uses metrics for which the distance between traces can have a gradient. It quantifies the degree to which the actual system model is close to the abstract one. The designers can decide what degree of closeness they desire. Exact trace inclusion may not be required as the model of the system may be only an approximation of the real world dynamics.
1Former Postdoctoral Researcher