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
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
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
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
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
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
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
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