Paper Abstract


Computational Models of Cellular Processing

Alex Bell, Mike Holcombe

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.


An integrated methodology for the formal specification, verification and testing of systems

Mike Holcombe

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


Almost All Software Testing is Futile!

Mike Holcombe, Florentin Ipate

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.


Another Look at Computability

Mike Holcombe, Florentin Ipate

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.


Using an X-Machine to Model a Video Cassette Recorder

M.Fairtlough, M.Holcombe, F.Ipate, C.Jordan, G.Laycock, Z.Duan

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.


X-machines with stacks and recursive enumerable functions

M.Holcombe, F.Ipate

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.


A testing method that is proved to find all faults

F.Ipate, M.Holcombe

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.


A simple prototype Visual Z environment

Mike Holcombe, Chih Nam Yap

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.


A seminar-based course that attemps to provide a more "academic" approach to software engineering

Mike Holcombe

The teaching of software engineering has evolved into a situation which emphasises the development of skills and understanding about the mechanics of carrying out large scale system design in a suitable environment. Although review and analysis are presented as parts of the development process there is often little emphasis on academic issues concerning a critical analysis and debate about the merits of the subject and approaches to it. Although software engineers will spend some of their professional life assessing other people's work, potential design methods and systems, we rarely focus on the process of assessment, per se in our courses.
Some of the important academic activities that take place during any process of learning at university include the collection and analysis of information, the understanding of concepts and processes, the examination of relationships and influences, the historical position of the subject, the making of informed judgments about the relative importance of contributions to the field and so on. No student of the humanities would be expected to "receive wisdom" in an uncritical way and part of the dynamism of these subjects is the continual questioning and rhetorical investigation of the works of leading proponents in the field. Little of that critical attitude seems to purvey the realms of current software engineering education.
We present here a discussion of an experimental course that we have developed to try to address some of these issues. The students on the course were required to prepare a lecture based on their reading of a recent paper from the Software Engineering literature. As well as explaining the ideas and results from the paper they were also asked to analyse it critically and assess it using clearly specified assessment criteria. The process brought out many interesting issues about the way software engineers attempt to justify their work and the great diversity of approaches taken to this task. These ranged from papers taking a detailed "scientific" approach using carefully designed experiments and proper statistical analysis through to papers that provided no justification or evidence that their approach worked, they either ignored giving any justification at all or based it on groundless assertions and hyperbole.
The critical appreciation of the software engineering journals by the students changed remarkably as we explored these ideas and tried to identify what the objectives of each paper were and whether they had achieved them.
This paper ends with two appendices, one is a list of the research papers studied, which might make a useful reference resource, and the second is an unedited example of one of the students' papers.


The "Crossover" software engineering project

Mike Holcombe

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.


Real life consultancy

Mike Holcombe

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.


Comprehension exercises - a new type of examination question

Mike Holcombe

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 Testing Strategies for Software Requirements and Design

Wachara Chantatub, Mike Holcombe

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.


This page was last modified on July 31 1995 by Chih Nam Yap.