and Testing Group
Mike Holcombe, (W.M.L. Holcombe), FBCS, C.Eng, FIMA, C.Math.
Professor of Computer Science, Head of Department of Computer
Dean, Faculty of Engineering 1999-2002.
Formal Methods of Design.
A number of EPSRC studentships will be available for PhDs in
2005/2006 these are restricted to UK residents. It is also possible
to apply for University fee waivers which can be used to offset some
of the fees for a PhD programme but students would still need to find
suppoirt for living costs. There are no scholarships available for
overseas students at present.
Microsoft Research are also offering PhD bursaries
in areas at the interface of computing and subjects like biology.
Other things of interest:
A picture of my
garden I am interested in growing unusual perennials and
alpines, if you share these interests please contact me.
Further information about The
University and Sheffield
Updated 5th May 1998.
Theory of Computing.
Theory of X-machines.
The theory of X-machines describes a fully general model of
computation. It provides a framework for the discussion of a wide
range of machine and language types ranging from classical finite
state machines to super-Turing machines. It has lead to a proposal
for a practical formal specification language for all types of
computational system, hardware, software, and hybrid control
systems. It has also provided the foundation for a theory of
(system) testing. The theory of
computational models based on X-machines has been described in
some detail. See the paper: "Another
look at computation."
Coworker: Florentin Ipate.
The theory of testing.
The need to carry out tests of systems - whether it is
fabrication testing of hardware (VLSI) or field testing of
communication systems or the testing of all manner of software
systems and components - is an essential but often neglected area
of computer and software engineering. The theory of testing is a
poorly developed area and the study of how to describe and reason
about testing activities is vital if we are to develop effective
testing strategies that are well founded. The theory of X-machines
is a convenient basis for this since it provides a computational
model within which testing processes can be discussed. For further
details of the theory of testing based on X-machines see a paper
"Almost all software
testing is futile."
Coworker is Florentin Ipate.
Formal Methods of Design.
Formal Specification Languages for Software Systems.
The principal interest is in the use of X-machines as a
language for describing software systems and the use of a formal
refinement mechanism for developing and extending the
specification. A number of case studies have been produced dealing
with systems such as graphical modelling tools, user interfaces of
CASE tools, word processors, operating systems etc.. as well as
Currently co-workers are Florentin Ipate,
Chih Nam Yap, Camilla Jordan, Matt Fairtlough.
The research is oriented around the use of communicating
X-machines for the specification of communications protocols and
This is joint work with Colin Smythe and
Formal Specification Languages.
The visual Z system is a prototype
visual formal specification environment. The idea is to replace
much of the mathematical symbolism of Z by more intuitive visual
icons and constructs and to provide a software system that will
support the development of Z specifications using visual methods
only. The hope is that this will make Z more accessible to the
software engineering industry. A prototype system has been built
and is being evaluated and extended. A related project involves the
automatic translation of natural language specifications into Z.
(Paul Mc Kevitt)
Collaborator this project is Chih Nam Yap.
Visual Proof Systems.
This is an experimental approach to replacing symbolic logic
with a pictorial system which allows for the development of proofs
using visual intuition. A simple case study developed within a
hypertext system has been built and is being evaluated. The origin
of the idea lies within cognitive science and the belief that the
visual system is capable of concurrent and exploratory reasoning
which might map onto the problem of identifying the tactics for
constructing a proof and of identifying the important intermediate
stages in the "route" between the premises and the
conclusion of a theorem.
Formal Specification Languages for Hardware Systems.
This subject was the focus of a joint SERC project with the
University of Hull, Department of Electronics (Professor Gaynor
Taylor). The use of X-machines for the specification of hardware
systems - primarily ASICs - was proposed. A formal specification of
a PID controller chip was reverse engineered from a layout design
and its functional behaviour was formally verified using the
X-machine approach. This work, done by Ringo Pang, was an excellent
demonstration of the power and simplicity of the high level formal
approach allowed by the X-machine method. Since then a number of
significant case studies have been carried out, the T8000
transputer was defined to a considerable level of detail using the
method. Currently the focus is on the comparison of the method with
existing approaches namely OBJ and HOL. The relationship with the
testing methods developed using X-machines is also important - see
Coworker is Florentin Ipate..
Test Set Generation for Software Systems including safety critical
A practical method of generating test sets from a formal
specification based on stream X-machines has been developed. This
method, formal test set generation,
provides guaranteed fault detection at the control space level. The
relationship between test generation and refinement has also been
explored. Some of the work (that relating to safety-critical
systems testing) is sponsored by Daimler-Benz AG Research
Coworkers are Kirill Bogdanov, Florentin
Ipate, Andreas Grondoudis and Gilbert Laycock (Leicester).
Test Set Generation for Hardware Systems.
This is a continuation of 2.5 whereby the formal specification
of the hardware as an X-machine provides the basis for test set
generation. The approach allows for the development of a design for
test approach and the functional fabrication test generation from a
Coworkers: Matt Fairtlough, Camilla
Jordan, Kirill Bogdanov, Florentin Ipate.
Integrated Design, Verification and Testing Methodologies.
A paper describing an integrated design
methodology based on X-machines is available (the full paper
may be consulted). This is an attempt to integrate the central
issues of system design within a coherent and theoretically
Specification and Verification of Hybrid Control Systems.
See the work on the formal specification of a hybrid
soaking pit. The work of Hybrid machines is also of importance.
Currently this is the subject of an EPSC funded research project
also involving the development of a hybrid temporal logic (2.10).
Coworker- Zhenhua Duan.
Interval Temporal Logic.
This logic provides the model theoretic basis for the hybrid
machines described in 2.9. It is based on an extension of Interval
Temporal logic with Projection (Duan) and provides a mechanism for
stating and proving results about the behaviour of real-time
systems involving both continuous processing and discrete events.
Coworker- Zhenhua Duan
Requirements capture and requirements testing.
This work involves the development of formal specifications,
written in an extended Z, from early design documents and
semi-formal diagramming techniques. The process of generating the Z
specification is mechanical. A simple proof theory has been
developed to provide for the verification of the consistency of
specifications between requirements and design. A paper was
presented at EuroSTAR94, Brussels.
Coworker - Wachara
Metrics for safety-critical systems.
This project is looking at a large database of project and
design information relating to a number of large, recent
safety-critical systems and is looking at the sorts of metrics that
provide the most useful information about the quality of the final
implementation of safety-critical code.
Coworkers are Tony Wood
Formal models of users and user interfaces.
This work is an attempt to provide a more formal basis for the
construction of user models and the incorporation of some of the
uncertainties associated with constructing general models of human
reasoning. The approach is founded on computational model
(X-machines) together with an involvement of belief logics to
provide a more realistic description of user behaviour based on the
user possessing a possibly incomplete or incorrect set of beliefs
about what the system does.
Coworker - Paul Mc Kevitt.
Computational models of Cellular Information Processing.
This area is concerned with the development of mathematical and
computational models of the information processing (essentially
biochemical activity) that is present in all living cellular
systems. The emphasis is at the cellular level and the modelling
method provides a language which can treat the internal structures
of the cell in an appropriate way and allows for the description of
what are essentially massively parallel computational systems.
Coworkers are Alex Bell and Ray Paton (Liverpool)
Modelling metabolic events and intra-cellular metabolism.
This project is a development of 3.1 focussing more on specific
metabolic pathways and the communication between such metabolic
Coworkers are Alex Bell and Ray Paton (Liverpool)
test set generation.
Abstract. Two current areas of emphasis in the development of
methods for engineering higher quality and safer software are the
use of formal methods for the specification and verification of
software and the development of sophisticated methods of software
and system testing. In general these two approaches are unrelated
and few examples exist whereby the best aspects of both are used in
an integrated way. This paper describes a method for using the
existence of a formal specification as the basis for the
development of a detailed functional software testing strategy.
(The specification can also be used as a basis for verification but
this is beyond the scope of the present article.) The method is
based on some recent theoretical advances in the theory of testing.
A simple case study is described which demonstrates the principal
idea. The formal method used has been chosen to be as intuitive and
as simple as possible in the hope that it will be usable in as wide
a range of software applications as possible and acceptable to as
wide a community of software engineers as possible.
models of a soaking pit and other hybrid and mixed mode systems.
Mike Holcombe, Zhenhua Duan.(CSRG),
Abstract. This paper describes a timed stream X-machine
specification of a hybrid control system based around a soaking pit
system in a steel works. Stream X-machines are a powerful general
specification language with a coherent theoretical foundation that
encompasses design refinement, formal specification, formal
verification and test set generation. The timed stream X-machine
allows for the explicit modelling of time, including specific time
intervals and exact time constraints. This paper describes how the
language can be extended to provide a specification for a dynamic,
hybrid control system. The formalism is intimately connected with
the provision of a logic and proof theory which enables
verification to be carried out in the model. The logic used is the
Hybrid Projection Temporal Logic (HPTL) described in .
simple prototype Visual Z environment.
Mike Holcombe & Chih Nam Yap,
Verification and Testing
Research Group, (VTRG)
Abstract. 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 examining 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 to obtain opinion and
suggestions which would lead to a better iconic environment for the
construction of Z specifications.
X-machines and recursively enumerable functions."
Florentin Ipate & Mike Holcombe (VTRG).
Abstract. 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 com- putational
capabilities and contrasts these with a number of other important
models. It is shown that a straight move stream X-machine computes
precisely the class of length preserving, partial recursive
functions. Other related results describing the computational
capability of stream X-machines are also presented.
Florentin Ipate and Mike Holcombe (VTRG).
KEYWORDS: State machine; Functional Testing; Formal
Abstract. Although a great deal of research has been done in
the area of formal methods and their practical use for
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 driven, therefore their validity cannot be
proved formally. This paper presents a theoretical testing strategy
based on the derivation of the test sets from the specification and
proves its validity. The type of specification used, the stream
X-machine, combines the control structure of a finite state machine
with an arbitrary data structure.
integrated methodology for the specification, verification and
testing of systems.
Mike Holcombe, (VTRG).
Abstract. 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.
position is challenged and a mechanism is proposed whereby:
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;
strategy is based on the derivation of test sets from formal
specifications (new generation functional testing).
KEYWORDS: State machine, Functional testing, Formal
specification, Verification, X-machine, Refinement.
Testing Strategies for Software Requirements and Design
Wachara Chantatub and Mike Holcombe, (VTRG).
Abstract. 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
A paper is
KEYWORDS: Structured Analysis and Design Methods, Z
Teaching theory of computer science.
Teaching theoretical material to undergraduates can be a
challenge and the way the material is presented and motivated are
crucial if the class is to obtain the maximum benefit and interest
from the exercise. We have introduced a number of innovations in
this area including extensive project oriented material and the
development of "comprehension" exercises and examination
Teaching software engineering to advanced students in a way
that encourages critical evaluation as well as developing technical
knowledge and skills is an urgent requirement today. Some
experiences in setting up a seminar based advanced course are
described in "A seminar-based course that attempts to provide
a more "academic" approach to software engineering."
(The full paper
may be consulted.)
Project work and industrial interaction.
Several project types are examined, the use of "live"
industrial clients in the context of a software hut exercise and
the Crossover project introducing first
year students to team working in the context of a software life
cycle model. (The full paper
may be consulted)
Another project involved students undertaking real consultancy
work in small local companies.
Abstract. We describe a project involving students carrying 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 strategy 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. (A paper may
Comprehension exercises - a new
type of examination question.
Abstract. 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. (A paper
may be consulted)
seminar-based course that attempts to provide a more "academic"
approach to software engineering.
Mike Holcombe, (VTRG)
Abstract. 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 the academic issues concerning a critical
analysis and debate about the merits of the subject and approaches
to it. In many areas of study there is great stress placed on a
number of important academic activities that take place during the
process of learning about the subject at university. These 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 attitude seems to purvey the realms of
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 reading 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. The 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 example of one of the students
papers. For further information the paper
may be consulted. See also some current
examples of student papers in the personal pages of colleague
This years course details can be found here.
"Crossover" software engineering project.
Mike Holcombe, (VTRG)
Abstract. The "Crossover" project is a first year
team project undertaken by all Computer Science and Software
Engineering 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
organisations; to gain experience of some the various stages of the
software lifecycle; to apply the methods and techniques for design,
implementation and testing of software discussed in their first
year courses; to provide some practical experience of project
management and quality issues and how these may be addressed and
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.
page was last modified on 7th July 1998.