Animation and Visualisation of Refinements

Robinson, Neil John (2005). Animation and Visualisation of Refinements PhD Thesis, Information Technology & Electrical Engineering, University of Queensland.

       
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
n01front.pdf n01front.pdf application/pdf 203.77KB 1
n02whole.pdf n02whole.pdf application/pdf 1.42MB 1
Author Robinson, Neil John
Thesis Title Animation and Visualisation of Refinements
School, Centre or Institute Information Technology & Electrical Engineering
Institution University of Queensland
Publication date 2005
Thesis type PhD Thesis
Supervisor Professor Colin Fidge
Abstract/Summary 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.
Keyword refinement
animation
abstraction relations
action systems
Z
data refinement

 
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 112 Abstract Views, 2 File Downloads  -  Detailed Statistics
Created: Fri, 21 Nov 2008, 16:54:20 EST