Verifying Trace Inclusion between an Experimental Frame and a Model

摘要

The concept of experimental frame is employed to define circumstances under which a model is simulated and observed. Verifying the applicability of an experimental frame to a model is a key step to ensure that the intended purpose of a simulation can be achieved. We assume that the specification of an experimental frame and a model are two software components in the formal sense. This paper suggests a component-based approach to build the right simulation used for system models verification and validation. We use Input/Output automata for components' behaviour specification. Behavioural signature is employed to specify the experimental frame and model capabilities. Then we formally define applicability conditions with matching rules to verify the trace inclusion between an experimental frame and a model. This approach is illustrated with an application study of an intelligent cruise controller.