Research Reports for 1998

CSR 1-98
Hierarchies of Spatially Extended Systems and Synchronous Concurrent Algorithms
M.J. Poole, J.V. Tucker and A.V. Holden
abstract    PDF
CSR 2-98
Providing Continuing Professional Development in Small to Medium Sized Enterprises
Beti Williams and G Manogg
abstract    PDF
CSR 3-98
Tensor Abstraction Programming of Computational Fluid Dynamics Problems
P.W. Grant, M. Haveraaen and M.F. Webster
abstract    PDF    PS
CSR 4-98
Second-order Hybrid Finite Element/Volume Method for Viscoelastic Flows
P. Wapperom and M.F. Webster
abstract    PDF
CSR 5-98
Design is a Document
Al Sadiq A. M. M. Halepota, P.W. Grant, and C. P. Jobling
abstract    PDF
CSR 6-98
Hierarchical Reconstructions of Cardiac Tissue
A.V. Holden, M.J. Poole and J.V. Tucker
abstract    PDF
CSR 7-98
Infinitary Algebraic Specifications for Stream Algebras
J.V. Tucker and J.I.Zucker
abstract    PDF
CSR 8-98
Algebraic Models of Correctness for Microprocessors
A.C.J. Fox and N.A. Harman
abstract    PDF
CSR 9-98
Simulation for Viscoelastic Flow by a Finite Volume/Element Method
P. Wapperom and M.F. Webster
abstract    PDF
CSR 10-98
A Study of Finite Volume Methods for Viscoelastic Flows
P. Wapperom and M.F. Webster
abstract    PDF
CSR 11-98
Language Preorder as a Precongruence
Wan Fokkink
abstract    PDF
CSR 12-98
Within ARM's Reach: Compilation of Left-Linear Rewrite Systems via Minimal Rewrite Systems
Wan Fokkink, Jasper Kamperman and Pum Walters
abstract    PDF
CSR 13-98
EURIS, a Specification Method for Distributed Interlockings
Fokko van Dijk, Wan Fokkink, Gea Kolk, Paul van de Ven and Bas van Vlijmen
abstract    PDF
CSR 14-98
Conservative Extension in Positive/Negative Conditional Term Rewriting with Applications to Software Renovation Factories
Wan Fokkink and Chris Verhoef
abstract    PDF
CSR 15-98
Verification of Interlockings:from Control Tables to Ladder Logic Diagrams
Wan Fokkink and Paul Hollingshead
abstract    PDF
CSR 16-98
Rooted Branching Bisimulation as a Congruence
Wan Fokkink
abstract    PDF
CSR 17-98
Towards an Algebraic Specification of the Java Virtual Machine
K. Stephenson
abstract    PS    PDF
CSR 18-98
Direct Rendering Algorithms for Complex Volumetric Scenes
Adrian LEU and Min CHEN
abstract    PDF
CSR 19-98
Constructive Volume Geometry
Min Chen and John V. Tucker
abstract    PDF
CSR 20-98
Algebraic Models of Superscalar Microprocessor Implementations: a Case Study
A.C.J. Fox and N.A. Harman
abstract    PDF
CSR 21-98
Algebraic Models of Temporal Abstraction for Initialised Iterated State Systems: An Abstract Pipelined Case Study
A.C.J. Fox and N.A. Harman
abstract    PDF
CSR 22-98
A Dynamic Docucentric Environment for System Design Support
Al Sadiq A. M. M. Halepota, P.W. Grant, and C. P. Jobling
abstract    PDF
CSR 23-98
JACIE - an authoring language for WWW-based collaborative applications
Abdul S. Haji-Ismail, Min Chen and Phil W. Grant
abstract    PDF

CSR 1-98 Hierarchies of Spatially Extended Systems and Synchronous Concurrent Algorithms

M.J. Poole, J.V. Tucker and A.V. Holden

First, we study the general idea of a spatially extended system (SES) and argue  that many mathematical models of systems in computing and natural science are  examples of SESs. We examine the computability and the equational definability  of SESs  and show that, in the discrete case, there is a natural sense in which  an SES is computable if, and only if, it is definable by equations. We look at a  simple idea of hierarchical structure for SESs and, using retimings and respacings, we define how one SES abstracts, approximates, or is implemented by another SES.  Secondly, we study a special kind of SES called a synchronous concurrent algorithm (SCA). We define the simplest kind of SCA with a global clock and unit delay  which are computable and equationally definable in easy ways by primitive recursive equations. We focus on two examples of SCAs: a systolic array for convolution and a non-linear model of cardiac tissue. We investigate the hierarchical structure of SCAs by applying the earlier general concepts for the hierarchical structure of SESs.  We apply the SCA hierarchy to the formal analysis of both the implementation of a  systolic array and approximation of a low level model of a cardiac tissue.
Report Titles


CSR 2-98 Providing Continuing Professional Development in Small to
Medium Sized Enterprises

Beti Williams and G Manogg

In order to assess the need and format of Continuing Professional Development in Information Technology (IT) in Small to Medium Sized Enterprises (SMEs) in the area of South Wales, a questionnaire has been devised.  30 SMEs have been interviewed and the results collected and analysed in this report.  We start with giving a brief summary of the methodology and analyse each section of the report in detail.  A summary conclusion is drawn at the end of the report.  It emerges that there is a perceived need for Continuing Professional Development in the area of IT, the most important constraint being time.
Report Titles


CSR 3-98 Tensor Abstraction Programming of Computational Fluid
Dynamics Problems

P.W. Grant, M. Haveraaen and M.F. Webster

It has long been acknowledged that scientific software is in need of better software engineering practices. Here we contrast the difference between conventional software development of CFD codes and an abstraction method based on tensor mathematics. The former approach leads to programs where different aspects, such as the discretisation technique and the coordinate systems, can get entangled with the solver algorithm. The latter approach yields programs that segregates these concerns into fully independent software modules. Such considerations are important for the construction of numerical codes for practical problems.
Report Titles


CSR 4-98 A Second-order Hybrid Finite Element/Volume Method for Viscoelastic Flows

P. Wapperom and M.F. Webster

A second-order accurate cell-vertex finite volume/finite element hybrid scheme is proposed. A finite volume method is used for the hyperbolic stress equations and a finite element method for the balance equations. The finite volume implementation incorporates the recent advancement on fluctuation distribution schemes for advection equations. Accuracy results are presented for a pure convection problem, for which fluctuation distribution has been developed, and an Oldroyd-B benchmark problem. When source terms are included consistently, second-order accuracy can be achieved. However, a loss of accuracy is observed for both benchmark problems, when the flow near a boundary is (almost) parallel to it. Accuracy can be recovered in an elegant manner by taking advantage of the quadratic representations on the parent finite element mesh.
Compared to the finite element method, the second-order accurate finite volume implementation is ten times as efficient.
Report Titles


CSR 5-98 Design is a Document

Al Sadiq A. M. M. Halepota, P.W. Grant, and C. P. Jobling

In this paper the document as a container environment paradigm is explored. Utilizing this paradigm a platform neutral prototype control system design environment is being developed which uses a document as the user interface. This document acts as the integrator of various tools. A JavaBeans component based solution, allows the environment to be extended and modified as needed.
Report Titles


CSR 6-98 Hierarchical Reconstructions of Cardiac Tissue

A.V. Holden, M.J. Poole and J.V. Tucker

We consider the general problem of comparing and integrating computational models of cardiac tissue at different levels of physiological detail. We use a general theory of synchronous concurrent algorithms to model spatially extended biological systems, and expand the theory to create hierarchical models by relating observable behaviour at different levels. The general concepts and methods are illustrated by a detailed study of electrical behaviour in cardiac tissue, in which models based on coupled systems of ordinary differential equations, partial differential equations and cellular automata are compared and combined.
Report Titles


CSR 7-98 Infinitary Algebraic Specifications for Stream Algebras

J.V. Tucker and J.I.Zucker

A stream is an infinite sequence of data from a set A. A wide variety of algorithms and architectures operate continuously in time, producing streams of data, for example: systolic arrays, data-flow machines, neural networks and cellular automata. Also many models of real number computation use streams. In this paper we study the construction of an algebra A- of streams over a many-sorted algebra A of data. In particular, we show how an initial algebra specification for A- can be constructed from one for A. One problem is that A- is uncountable even when A is finite. To handle this, we work with infinitary terms called stream terms, and infinitary formulae that generalise conditional equations, called w-conditional stream equations.
Report Titles


CSR 8-98 Algebraic Models of Correctness for Microprocessors

A.C.J. Fox and N.A. Harman

In this paper we present a method of describing microprocessors at different levels of temporal and data abstraction. We consider microprogrammed, pipelined and superscalar processors, in which instructions may complete simultaneously, or out of program order.

We model microprocessors by means of iterated maps. These maps are defined by equations which evolve a system from an initial state by the iterative application of a next-state function. A formal model of time is used in the form of a clock algebra. Time is related by temporal abstraction maps called retimings. We state correctness conditions for microprogrammed, pipelined and superscalar microprocessors. We introduce and prove the one step theorem that permits verification of correctness conditions to be considerably simplified under well-defined conditions.
Report Titles


CSR 9-98 Simulation for Viscoelastic Flow by a Finite Volume/Element Method

P. Wapperom and M.F. Webster

Stability of a second-order finite element/finite volume hybrid scheme is investigated on the basis of flows with increasing Weissenberg number. Finite elements are used to discretise the balances of mass and momentum. For the stress equation a finite volume method is used, based on the recent development with fluctuation distribution schemes for pure convection problems. Examples considered include a start-up channel flow, flow past a cylinder and the non-smooth 4:1 contraction flow for an Oldroyd-B fluid. A considerable gain in efficiency per time step can be obtained compared to an alternative pure finite element implementation. A distribution based on the flux terms is unstable for higher Weissenberg numbers, and this is also true for a distribution based on source terms alone. The instability is identified as being caused by the interaction of the balance equations and stress equation. A combination of distribution schemes based on flux and source terms, however, gives a considerable improvement to the hybrid FE/FV implementation. With respect to limiting Weissenberg number attenuation, the hybrid scheme is more stable than the pure finite element alternative for the smooth flow past a cylinder, but less so for the non-smooth contraction flow. The influence of additional strain-rate stabilisation techniques is also analysed and found to be beneficial.
Report Titles


CSR 10-98 A Study of Finite Volume Methods for Viscoelastic Flows

P. Wapperom and M.F. Webster

This study investigates the application of a new hybrid finite element/finite volume scheme to the numerical solution of some viscoelastic flows. Such an FE/FV approach is contrasted against a purely finite element alternative, that has previously been developed to address highly elastic problems. For incompressible viscoelastic flows, with non-trivial source terms, the question arises as to whether a finite element approach may be best suited to solve for the parabolic field equations, concerned with the conservation of mass and momentum, whilst a finite volume approach may be more appropriate for the hyperbolic constitutive law, as originally devised. For example, recent work on advection equations has shown that fluctuation distribution schemes that handle upwinding for fluxes, can yield accurate solutions for problems that manifest steep gradients. Efficiency, accuracy and stability are the prime considerations, to be achieved through a localised control volume view, high resolution TVD-type schemes and oscillation-free transient solutions. Computational tractability follows as a consequence.
Report Titles


CSR 11-98 Language Preorder as a Precongruence

Wan Fokkink

Groote and Vaandrager introduced the tyft format, which is a congruence format for strong bisimulation equivalence. This article proposes additional syntactic requirements on the tyft format, extended with predicates, to obtain a precongruence format for language preorder.
Report Titles


CSR 12-98 Within ARM's Reach: Compilation of Left-Linear Rewrite Systems via Minimal Rewrite Systems

Wan Fokkink, Jasper Kamperman and Pum Walters

A new compilation technique for left-linear term-rewriting systems is presented, where rewrite rules are transformed into so-called minimal rewrite rules. These minimal rules have such a simple form that they can be viewed as instructions for an abstract rewriting machine (ARM).
Report Titles


CSR 13-98 EURIS, a Specification Method for Distributed Interlockings

Fokko van Dijk, Wan Fokkink, Gea Kolk, Paul van de Ven and Bas van Vlijmen

Safety systems for railways have shifted from electronic relays to more computer-oriented approaches. We present a tutorial on the EURIS method from NS Railinfrabeheer, which champions an object- oriented approach to the specification of interlocking logics. We also give an overview of UniSpec, which is an instance of EURIS for the Dutch railway system.
Report Titles


CSR 14-98 Conservative Extension in Positive/Negative Conditional Term Rewriting with Applications to Software Renovation Factories

Wan Fokkink and Chris Verhoef

We transpose a conservative extension theorem from structured operational semantics to conditional term rewriting. The result is useful for the development of software renovation factories, and for modular specification of abstract data types.
Report Titles


CSR 15-98 Verification of Interlockings:from Control Tables to Ladder Logic Diagrams

Wan Fokkink and Paul Hollingshead

Dependency relations between objects in a railway yard are tabulated in control tables. An interlocking, which guarantees validity of these dependencies, can be implemented in ladder logic. We transform a ladder logic diagram into a Boolean formula, so that validity of the dependencies in the control tables can be verified using a theorem prover. Time copies and invariants are added to the formula, to relate it more firmly to its ladder logic diagram. Program slicing is applied to reduce the size of the formula.
Report Titles


CSR 16-98 Rooted Branching Bisimulation as a Congruence

Wan Fokkink

This article presents a congruence format, in structural operational semantics, for rooted branching bisimulation equivalence. The format imposes additional requirements of Groote's ntyft format. It extends an earlier format by Bloom with standard notions such as recursion, iteration, predicates, and negative premises.
Report Titles




CSR 17-98 Towards an Algebraic Specification of the Java Virtual Machine

K. Stephenson

We develop an algebraic specification of the architecture of an abstract and simplified version of the Java Virtual Machine (JVM). This concentration on the implementation-independent features of the machine allows us to build a clean and easily comprehensible model in which its structure is emphasised. We then axiomatise the semantics of programs on this architecture. We also consider how we can concretise this abstract model which provides us with a firm foundation for exploring the entire JVM and thus of analysing the correctness of Java implementations.
Report Titles


CSR 18-98 Direct Rendering Algorithms for Complex Volumetric Scenes

Adrian LEU and Min CHEN

This paper concerns a new sub-field of computer graphics, namely volume graphics, which aims to develop voxel-based modelling and rendering techniques for general purpose graphics in addition to its original playing field, volume visualisation. Building upon our recent work on the modelling of graphics scenes composed of multiple volumetric datasets, we present three different algorithms for rendering such scenes. The results have shown that traditional single-volume rendering methods, such as direct volume rendering by ray-casting and splatting, can be effectively extended to multi-volume environments. The work has thereby demonstrated the feasibility and the potential of using voxel-based representations in computer graphics.
Report Titles


CSR 19-98 Constructive Volume Geometry

Min Chen and John V. Tucker

Having evolved from volume visualisation, volume graphics is emerging as an important sub-field of computer graphics. This paper focuses on a fundamental aspect of volume graphics, the modelling of complex graphics objects and scenes using volume data types. We present an algebraic theory for volume data types, and describe a hierarchical modelling scheme, called Constructive Volume Geometry (CVG), for building complex volume objects. We also outline a recursive algorithm for rendering scenes composed of CVG objects. The work has demonstrated the feasibility of using volume data types in general graphics applications, and the advantages of volume data types over surface/solid data types in some aspects.
Report Titles


CSR 20-98 Algebraic Models of Superscalar Microprocessor Implementations: a Case Study

A.C.J. Fox and N.A. Harman

We extend a set of algebraic tools for microprocessor to model superscalar microprocessor implementations, and apply them to a case study. We develop existing correctness models to accommodate the more advanced timing relationships of superscalar processors, and consider formal verification. We illustrate our tools and techniques with an in-depth treatment of an example superscalar implementation.

Clocks divide time into (not necessarily equal) segments, defined by the natural timing of the computational process of a device. We formally relate clocks by surjective, monotonic maps called retimings. In the case of superscalar microprocessors, the normal relationship between `architectural time' and `implementation time' is complicated by the fact that events that are distinct in time at the architectural level can occur simultaneously at the implementation level.
Report Titles


CSR 21-98 Algebraic Models of Temporal Abstraction for Initialised Iterated State Systems: An Abstract Pipelined Case Study

A.C.J. Fox and N.A. Harman

The data and temporal abstractions of an abstract pipelined case study are explored in an algebraic setting. We apply a set of algebraic tools to the specification, pipelined implementation, and formal verification of an abstract case study. We employ a model of time based on counting events by means of a clock. We relate different levels of timing abstraction, or clocks, by surjective, monotonic maps called retimings. We model systems as iterated maps that evolve over time from some initial state. We define formal correctness conditions, and introduce the one-step theorems that, given certain conditions, reduce the complexity of formal verification. The algebraic models provide: (i) modular descriptions of pipelined systems, including correctness criteria; and (ii) equational specification and verification techniques for the design of pipelined systems applicable to a range of specification languages and theorem provers.
Report Titles


CSR 22-98 A Dynamic Docucentric Environment for System Design Support

Al Sadiq A. M. M. Halepota, P.W. Grant, and C. P. Jobling

WWW has prompted development of diverse technologies such as Java, HTML, XML etc. to enable presentation and propagation of information via documents and their active contents. Documents on the web present themselves as the containers of the various kinds of media to transfer information. This has provided a springboard for Java to quickly become a popular language, not only for designing web pages with active contents, but also for developing cross platform applications. This paper presents the work done by the authors to implement an environment for computer aided system design using a document centric paradigm. This environment has been developed in Java and takes advantage of Java's ability to instantiate objects from their string name descriptors at run time. This has allowed a creation of a fully extensible and modifiable environment, in which a design task at hand is described as a document. This document is marked-up using eXtensible Markup Language (XML). The advantage of using XML is that it provides descriptions of data structures and allows us to define our own tags to describe document elements and their attributes. Different elements of the document are handled by small components based on the Java Beans model but their integration is performed at run time without explicit need for connection or adapter class compilation thus allowing user modification without relying on a Java Bean builder environment. Several components have been built to assemble a formatted document. Special components have also been implemented to provide bridges between applications such as MATLAB etc. An XML Document Type Definition (DTD) has been provided to allow for valid and well-formed documents. The development of this environment has afforded us a designing experience, which takes advantage of current web-based technologies and their integration with classical design and simulation tools. We hope to provide users of this environment, a solution for design, documentation and extension in an integrated system, which can be easily scaled to take advantage of the next wave of web based objects
Report Titles


CSR 23-98 JACIE - an authoring language for WWW-based collaborative applications

Abdul S. Haji-Ismail, Min Chen and Phil W. Grant

With continuous acceptance of WWW as a de facto standard for human- computer interaction and human-human communication, it is desirable to develop collaborative applications under the framework of WWW. In this paper, we present a new script language called JACIE, which is designed to support rapid implementation of a wide range of multimedia collaborative applications. In particular, we highlight the necessity to support the management of interaction and communication activities in collaborative applications, and describe how JACIE facilitates such support through the concepts of channels and interaction protocols. JACIE also features a template-based programming style, a single program for both client and server, and platform-independence by using Java as the target language.
Report Titles