WiP abstract: Conformance testing as falsification for cyber-physical systems

In a typical Model-Based Design (MBD) process for Cyber-Physical Systems, an initial 'simple' Model is successively refined and made more accurate and complex; then it is implemented on a real-time computational platform, and further modified to yield an Implementation. The goal is to produce a system that satisfies a formal specification Φ. This successive refinement raises the question of how 'close' are the 'simple' Model and the'complex'Implementation. Answering this question is important because it is not always possible to verify formally that the Implementation satisfies the specification Φ. Moreover, even if the Implementation satisfies Φ, it will have unspecified behavior which might exhibit bugs. By quantifying the 'closeness' between Model and Implementation, our level of confidence in the Implementation derives from our confidence in the Model, and the fact that the Model satisfies Φ.