A number of simple algebraic models have been developed for the representation of basic metabolic processing and related activities in cells. These tend to make gross assumptions about a number of vital aspects of these complex dynamic systems. We present a hierarchical model based on a general theory of computation which sets out to model these systems without making many of these assumptions. We concentrate then on modelling the specific resource-based local metabolic processing that lies at the bottom of this hierarchy.

The practical use of formal methods in the specification and verification of software systems is an area where the UK and Europe have a significant competitive edge and from the point of view of research there has been much emphasis on this area. However, little of the work also addresses testing issues - there is almost an implication that testing is unnecessary when a system has been formally developed and certainly testing issues are very rarely discussed by those involved in formal methods. This position is challenged and a mechanism is proposed whereby: testing is integrated more fully into the design process and, in particular, is considered at the beginning of the life cycle; there is the potential that as the design is refined and transformed into an implementation the top level, abstract test strategy is similarly transformed into detailed test sets; The test strategy is based on the derivation of test sets from formal specifications (new generation functional testing).

All software systems are subject to testing - for some of them testing is the major activity in the project. Testing, however, rarely gets the attention it deserves from researchers and developers, partly because its foundations are very weak and ill-understood. The principal purpose of testing is to detect (and then remove) faults in a software system. A number of techniques for carrying out testing, and in particular, for the generation of test sets exist. Many sophisticated (and expensive) tools are available on the market and many look to these to provide a solution to the problems of building fault-free systems. We consider the problem of fault detection and note that few, if any, of the existing methods really address the real issues. In particular no methods allow us to make any statement about the type or precise number of faults that remain undetected after testing is completed. Thus we cannot really measure the effectiveness of our testing activities in any rigorous way. However, by considering testing from a straightforward, theoretical point of view we demonstrate that a new method for generating test cases can provide a more convincing approach to the problem of detecting ALL faults and allows us to make sensible claims about the level and type of faults remaining after the testing process is complete.

The theory of computable functions is well known and has given rise to many classes of computational models of varying power and usefullness. We take another look at this subject using the idea of a generalised machine - the X-machine - to provide some further insights into the issue and to discuss an elegant general approach to the question of classifying computational models including some of the so called "Super-Turing" models. This paper investigates a number of classes of X-machines. It considers their relative computational capabilities and contrasts these with other important models. It is shown that a certain class of these machines - the 2-stack straight move stream X-machine - computes precisely the class of partial recursive functions. The importance of this work to the theory of testing of systems is stressed.

The problem of constructing a simple formal specification of a dynamic, time dependent system is addressed here. We use an intuitive state machine model which can be developed in a series of stages, each successive refinement adding new features and addressing new issues related to the design of the specification. The model used in fully general, unlike traditional state machine models, and can be supported by a test generation method that will provide a basis for an integrated design for test specification method. The case study is the specification of a video cassette recorder system which is defined in a formal way with the minimum of mathematical notation.

This paper introduces the classes of X-machines known as stream X-machines, straight move stream X-machines and X-machines with stacks. It considers their relative computational capabilities and contrasts these with other important models. It is shown that a 2-stack straight move stream X-machine computes precisely the class of partial recursive functions. Other related results describing the computational capability of stream X-machines and straight move stream X-machines with stacks are also presented.

Although a great deal of research has been done in the area of formal methods and their practical use for the specification and verification of software systems, testing issues are very seldom mentioned by those within the formal methods community. Almost all the methods currently used for testing software are experience based rather than theoretically founded methods. In particular, very few methods allow us to make any statement about the type or number of faults that remain undetected after testing is completed. This paper describes a method for using the existence of a formal specification as the basis for the development of a detailed functional testing strategy. By considering testing from a theoretical point of view we demonstrate that this method can provide a more convincing approach to the problem of detecting all faults. The formal method used, X-machines, is a blend of finite state machines, data structures and processing functions and provides a simple and intuitive way for specifying computer systems.

Formal specification languages, such as Z, are perceived to be difficult to use and are consequently unpopular in industrial software design teams. We have been examinging ways in which the symbolic mathematical notation can be replaced by intuitive visual images and icons in a coherent and practical way without sacrificing rigour and the formal underlying semantics, This report looks at a prototype experimental Visual Z system and evaluates it in the light of the expectations and requirements of software designers. We are seeking opinion and suggestions which would lead to a better iconic environment for the construction of Z specification.

The "Crossover" project is a first year team project undertaken by all Software Engineering, Computer Science and dual students in the Department. It aims to highlight some of the practical issues that face all software development teams concerning the development of software systems in a large organisation; to gain experience of some of the stages of the software lifecycle; to apply the methods and techniques for design, implementation and testing of software discussed in their first year courses; and to provide some practical experience of project management and quality issues and how these may be addressed. It also provides an exciting environment for the development of skills in group working. We examine the development of the project, its main features and its position in our curriculum. We also evaluate its success, as far as possible.

We describe a project involving students carring out a real consultancy exercises with local companies, in which the students played the role of IT consultants and assessed a company's business, the scope for applying information technology in the company and developed a properly researched and costed proposal for the implementation of an IT stratefgy for the company. We look at how this was organised, how the students performed, what the companies thought and the benefits for the students' educational experience.

For many subjects in the arts area, particularly languages, comprehension exercises are a fundamental aspect of the teaching of the subject. So that students will be given a passage of prose or a poem which they have probably not seen before and then asked a number of questions about it to test their understanding of it, to ask them to critically analyse the passage and perhaps to develop some of the ideas and themes further. Since much of Computer Science is also language based, particularly in the realms of formal methods and the theory of computation, the issue of comprehension, criticism and development are also vital issues. We have been introducing comprehension exercises into some of our examinations in order to develop and assess these skills explicitly. In fact we have been doing this since 1988 and the conclusions from this, together with some examples of examination papers, are given.

Software requirements testing and software design testing are very important and must be taken seriously. Specifications of software requirements and design must be verified and validated before the implementation. Many individuals involved in design still find that some of the techniques available for these tasks are difficult and far from practical. This paper presents simple and very practical techniques for these tasks. The suggested techniques emerge from integrating three specification techniques, namely an informal specification technique (English language), a semi-formal specification technique (graphical models, namely entity-relationship diagram, data flow diagram, and data structure diagram), and a formal specification technique (a slightly extended version of the language Z). The three techniques mentioned above are very useful for different aspects and by using all of them in combination will provide practical and efficient techniques for the above mentioned tasks. However, by just simply using them as usual does not provide satisfactory results, therefore, we adapt and modify them to achieve software requirements and design specifying and testing techniques that are capable of providing satisfactory results. In this paper, we discuss: 1) how to draw the diagrams, we will suggest new ideas of how to draw the diagrams; 2) how to write formal specifications for software requirements and design, we will suggest new ideas of how to write formal specification using the extended Z specification language; 3) how to apply informal and formal proofs to verify and validate software requirements specification and software design specification; 4) the procedures of some of the tasks concerned. We do believe that the suggested techniques will be found useful, not too difficult, and efficient, especially for business information systems.