Case Studies

  The two primary areas of case study activity were the Algebraic Structure of Computers (A C Fox, N A Harman and J V Tucker), and the representation of Dynamical Systems (J V Tucker, in conjunction with A V Holden and M Poole at the University of Leeds).

[Harman, Tucker 95a]

N A Harman and J V Tucker, Algebraic models of microprocessors: architecture and organisation, Acta Informatica, 1995 (to appear)

[Harman, Tucker 95b]

N A Harman and J V Tucker, Algebraic models of microprocessors: the verification of a simple computer, University of Wales Swansea, Computer Science Report CSR 1-95, 1995.

[Fox, Harman 95]

A C Fox and N A Harman, Algebraic models of microprocessors: representation of advanced structures, in preparation.

Work on the Algebraic Structure of Computers has focussed on a detailed examination of two small case studies, including representations at two levels of abstraction, correctness conditions between these levels, and outline verification ([Harman, Tucker 95a], [Harman, Tucker 95b]). In particular, the verification process is significantly simpler than that normally associated with devices of such complexity. Also, work has proceeded on the development of algebraic tools for representing advanced aspects of computer design, including pipelined and superscalar architectures ([Fox, Harman 95]). In addition, a number of real-life example architectures (DEC Alpha, Motorola 68000, Berkeley RISC II, SUN Sparc) have been studied, as selected student's projects, to evaluate the practical applicability of the algebraic techniques developed. Future work will:

• extend the algebraic tool-set to work with further advanced features of modern processors; and
• develop a software environment to partially automate the verification of large examples (based on existing theorem proving and proof checking tools).

[Poole 95]

M Poole, Synchronous Concurrent Algorithms and Dynamical Systems, University of Wales Swansea, Department of Computer Science PhD Thesis, 1995

[Holden et al. 94]

A V Holden, M Poole, J V Tucker and H Zhang, Coupling CMLs and the synchronization of a multilayer neural computing system, Chaos, Solitons and Fractals 4, 1994, pp. 2249 -- 2268

Work on Dynamical Systems has focussed on the development of formal techniques for representing models of Cellular Automata and Coupled-Map Lattices within the algebraic model of Synchronous Concurrent Algorithms (SCAs), the development of software tools to simulate Dynamical Systems within the framework of SCAs, and the application of SCA-based Dynamical Systems Models to real-world problems (in particular, whole heart modeling. See [Poole 95], [Holden et al 94]. SCA-based models of Dynamical Systems have a number of advantages over existing approaches, including the formulation of correctness conditions.