Animation and Visualisation of Refinements

Specification animation has become a popular technique in industry, particularly for validation in model-based design processes. Animation tools provide the ability to explore and visualise the behaviour of a model without needing to study its internal workings. Formal refinement techniques should also be of interest to industry since they support verifiably correct transformations of system models towards implementation. So far, however, refinement techniques are not widely used. Their application requires a high degree of mathematical skill, even with the currently available tool support. Better tool support is needed to make refinement techniques accessible to industry. In this thesis we investigate the application of existing specification animation and visualisation tools to problems in refinement theory. We show how animation and visualisation can be used to support verification, by refinement, and validation, by comparing the behaviour of a refined specification against its abstract specification. Such techniques can be used to explain and/or improve the understanding of a refinement and to check for the presence of errors in a refinement, for example, before attempting a proof. In the most challenging cases, data refinements, the designer needs to supply an abstraction relation in order to prove the refinement. We initially assume that an abstraction relation is provided as an input to the verification and validation tasks. However, finding abstraction relations is hard, and is currently a matter of trial and error. We therefore study the problem of finding abstraction relations. We show that, if an abstraction relation exists, there is always a unique weakest abstraction relation and at least one minimal abstraction relation, and we describe algorithms for finding both the weakest abstraction relation and minimal abstraction relations. These algorithms can be applied to small finite-state systems to produce abstraction relations in terms of explicit values of state variables. We then investigate a symbolic algorithm for finding abstraction relations, which can be applied to systems with infinite states, to produce abstraction relations in predicate form. The theory and the algorithms we develop thus make it possible for us to extend our animation-based verification and validation techniques so that they can be used without providing a complete abstraction relation. Additionally our extended techniques can help a designer construct an abstraction relation or check a proposed one