Department of Computing Seminars 1998/1999

Dependence Analysis of Concurrent Programs and Systems
Tuesday 1st September 1998 - Professor Jingde Cheng, Kyushu University, Japan:
In this talk, I survey the program dependence analysis technique for concurrent programs and its applications from the viewpoint of software engineering. I present various primary program dependences which may exist in a concurrent program, a general approach to define, analyze, and represent these program dependences formally, and applications of an explicit program dependence representation for concurrent programs in various software engineering activities. I also suggest some research problems on dependence analysis of concurrent systems.

Algebraic Specifications: Assessing their Quality and their Effectiveness in Specification-based Testing
Tuesday 29th September 1998 - Dr Martin Woodward, Liverpool University:
There is an increasing trend towards more formality in the development of specifications of software systems in order to reduce the likelihood of errors as early as possible in the development process. The algebraic approach to specification, with its equational form, leads to the added advantage of executability via the process of term-rewriting. Nevertheless, algebraic specifications themselves may be developed which are erroneous or simply of poor quality. This talk will focus on pragmatic techniques and tools to test algebraic specifications and to assess their structural quality. Also, brief mention will be made of some empirical work to assess the effectiveness of test data that is automatically generated from algebraic specifications for testing equivalent procedural implementations.

Predicting Test Effectiveness
Tuesday 20th October 1998 - Dr Marc Roper, Strathclyde University:
Testing is an essential component of the software development process, but also one which is difficult to control. It is well understood that testing techniques are not guaranteed to detect all faults, but more frustrating is that after the application of a testing technique, the tester has no knowledge of how many faults might still be left undiscovered. Recently, capture-recapture models have been applied to software inspection data to predict the number of defects remaining in a document after inspection. However, there are significant differences between the inspection and testing processes and so it is not safe to assume that such techniques will be as successful in the testing domain. This talk investigates the applicability of capture-recapture models to testing by taking into consideration the characteristics of the testing process and comparing the performance of the various existing models. The models are evaluated with empirical data from studies which compared the relative merits of different testing techniques, and the factors effecting the accuracy of the models are analysed.

When are Hard Problems Genuinely Hard? An Introduction to Phase-transition Phenomena and the Implications for Efficient Algorithms
Tuesday 27th October 1998 - Dr Paul Dunne, Liverpool University:
All of the classical examples of computational problems for which only inefficient and infeasible algorithms are known, seem to reduce to the general problem of searching a given structure, such as a graph, in order to decide if the structure possesses a particular property of interest, e.g. does a graph contain a path which visits each graph vertex exactly once? The major weakness of the known methods for addressing certain important search problems of this type is that they effectively come down to considering all possible candidate solutions in turn until it can be decided that either an appropriate solution exists or that no solution is possible. Thus, in the path example, the best known methods must, in the worst-case, consider about n! candidate paths in deciding if an n-vertex graph possesses a path of the required form. This, however, does not mean that every n- vertex graph requires such inordinate search times: clearly a graph with no edges at all cannot have an appropriate path; equally a graph in which every possible edge is present, trivially, has such a path. The phenomenon of search problems, known as a phase- transition, deals with these two extreme behaviours in a rather more sophisticated way: informally, it is clear that the existence or non-existence of a suitable path is partly determined by whether the graph has or does not have `enough' edges. In fact, it turns out that we can very precisely characterise the threshold which determines the meaning of `enough', i.e. for a `typical' n-vertex graph with m edges it is known that if mf(n) then the graph `almost certainly' has a suitable path: furthermore, for this particular problem, the function f(n) is known exactly. Knowledge concerning how a `typical' graph behaves has turned out, in several cases, to be sufficient to allow the construction of algorithmic solutions which, although not always efficient, are provably fast `on average' for appropriate inputs. Similar behaviours have been observed for a very wide range of hard combinatorial search problems (not just for graphs). In this talk an introduction to the concept of phase- transition phenomena is given. After a brief review of some classical results, some approaches to studying and applying such phenomena will be presented together with a survey of a number of open issues in the field. Several of these are the object of study of an EPSRC. Research Grant awarded under the MathfIT initiative to a team in the Department of Computer Science at Liverpool.

Using Real Paper To Communicate with Computers
Tuesday 10th November 1998 - Professor Heather Brown, University of Kent at Canterbury:
This talk covers two novel methods of using paper to communicate with computers. Both are designed to allow paper to become an active part of a computer system. The first method involves the use of a computer-enhanced desk known as a DigitalDesk. The DigitalDesk can recognise pages placed on the desktop and can match them up with corresponding electronic versions. This allows users to access or manipulate information in the electronic version via natural actions such as pointing at text on the page. I shall describe the `Active Alice' project which used a DigitalDesk to turn a normal paperback version of `Alice's Adventures in Wonderland' into an integral part of a grammar lesson for students. The second method uses Xerox's `intelligent paper'. This looks like ordinary paper but contains invisible information that can be detected by a special pointer device. I shall outline the mechanisms used for intelligent paper and describe some potential applications.

Linking informal and formal requirements: a tool based on the B-Toolkit and DOORS.
Tuesday 1st December 1998 - Dr Jeremy Dick, Quality Systems & Software Ltd, Oxford:

On the rank of random matrices over finite fields
Tuesday 8th December 1998 - Dr Colin Cooper, University of North London:

Topological Design Theory
Tuesday 26th January 1999 - Professor Mike Grannell, Open University:
Embedding a graph in a surface produces faces. These faces may be regarded as the blocks of a combinatorial design. Given the general difficulty of effecting such embeddings, it is perhaps not surprising that the design-theoretical aspect seems to have hitherto attracted little attention. In his book on the solution of the Heawood conjecture (\textit{Map Color Theorem}, Springer-Verlag, 1974), Gerhard Ringel describes embeddings of the complete graph $K_n$ in orientable surfaces of minimal genus. It was recently shown that his solution for $n\equiv 3$ (mod 12) produces a face 2-colourable triangulation of $K_n$ whose faces (in each colour) correspond to the well-known Bose construction for Steiner triple systems. Again, until recently, very few nonisomorphic minimal genus embeddings of $K_n$ were known for each $n$ (I think three was the record for orientable surfaces). In this talk I will describe some recursive constructions for topological embeddings which correspond to known recursive constructions for block designs. They facilitate the construction of large numbers ($2^{O(n^2)}$) of nonisomorphic minimal genus embeddings of $K_n$ for $n$ lying in certain residue classes. I will then discuss work in progress, some open problems and some conjectures which have arisen. This is joint work with Geoff Bennett, Paul Bonnington, Terry Griggs and Jozef \v Sir\' a\v n.

Testing Refinements of State-based Formal Specifications
Tuesday 2nd February 1999 - Dr John Derrick, University of Kent at Canterbury:
A specification provides a concise description of a system, and can be used as both the benchmark against which any implementation is tested, and also as a means to generate tests. Formal specifications have potential advantages over informal descriptions because they offer the possibility of reducing the costs of testing by automating part of the testing process. This observation has led to considerable interest in developing test generation techniques from formal specifications, and a number of different methods have been derived for state based formalisms such as Z, B and VDM. However, after tests have been derived from a formal specification, the specification might be refined further before its implementation, and therefore a mechanism is needed to relate the abstract tests to the refined implementation. This talk describes such a method by exploring the relationship between testing and refinement. The test generation model we use constructs a finite state machine (FSM) from a Z specification by using a DNF partition analysis of the state and operations. The finite state machine is then used to derive suitable test suites. We describe a way of calculating a FSM for a refinement from an abstract FSM together with the information about the refinement embodied in the retrieve relation. This means that it is possible to test an implementation by generating a new concrete finite state machine from a set of abstract tests.

Hierarchies of program schemes
Tuesday 9th February 1999 - Professor Iain Stewart, Leicester University:
Finite model theory, that is, the study of the expressive power of logics on finite structures, is a thriving research area mid-way between mathematics and computer science. Descriptive complexity theory is one aspect of finite model theory dealing explicitly with the relationship between computational complexity theory and finite model theory. Typical results in descriptive complexity theory are Fagin's Theorem that NP is the class of problems definable by sentences of existential second-order logic, and the Immerman-Vardi theorem that P is the class of problems on ordered structures definable by the sentences of least-fixed point logic. It is unknown whether there exists a logical characterization of any complexity class "below" NP on the class of all finite structures (and not just the class of ordered structures). In this talk I shall introduce simple classes of program schemes and relate these program schemes with well-known logics in descriptive complexity theory (these program schemes are actually just extended while-programs taking finite structures as input). I will prove that there are proper infinite hierarchies within these classes of program schemes which translate to corresponding logical hierarchies on the class of all finite structures (even when we restrict the class of problems to problems only involving trees). The talk will be suitable for non-experts in the field.

Design for test
Tuesday 16th February 1999 - Professor Mike Holcombe, Sheffield University:

Re-engineering: One approach to Coping with Constant Software Changes
Tuesday 9th March 1999 - Dr Hongji Yang, De Montfort University:
With the advent of new architectures, the need to introduce new functionalities and the improvement in design techniques, there is a strong need to re-engineer existing software systems maintaining their continuity of use.
By re-engineering, we adopt the view of examining and altering an existing subject system to reconstitute it in a new form. This process encompasses a combination of various sub-processes, mainly reverse engineering and forward engineering.
Our recent research in the Software Research Technology Laboratory aims to develop an integrated and practical approach that handles compositional analysis and the constant change in system requirements. Issues addressed include program transformation for restructuring, abstraction for reverse engineering, componentising reusable code, formalising an Object-Oriented development approach, migration to CORBA and measuring reverse engineering. Our views to above issues are discussed in the seminar.

Optimisation Based Approaches to the Synthesis of Hard Real Time Systems
Tuesday 16th March 1999 - John Clark, York University:
Developing safety critical real-time systems is hard – very hard. Most design techniques and methods of refinement deal predominantly with (so-called) functional requirements. Safety critical systems also have to satisfy crucial non-functional properties, e.g. hard time constraints. One would like to be able to generate designs at various levels that make best use of available components (or intended components with postulated properties) taking into account required system reliability, the ability to meet all deadlines and costs of development/maintenance etc. In this talk, some recent work by Nicholson, Burns and Clark on the EPSRC-funded DESSERTS project is reported which uses heuristic optimisation techniques to generate putative solutions to system design problems. The work encompasses various levels: architectural synthesis and task allocation over available processors, and fuses the facilities of best available quantitative reliability modelling tools (SHARPE) and schedulability analysis developed at York by the Real Time Systems Group.

Tuesday 23rd March 1999 - Richard Pearce, Wye College:

Jordan approach to representations of the Lorentz group
Tuesday 30th March 1999 - Professor Bernie Russo, University of California:

Engineering and re-engineering software for change
Tuesday 27th April 1999 - Professor Keith Bennett, Durham University:
I'd like to present results from a 10 year research project on the application of formal methods to the reverse engineering of industrial scale software. We have used a transformation-based system to obtain design abstractions from real source code, written in languages such as Assembler and Jovial! This work has stimultated many theoretical problems as well as practical issues in developing good tool support. At the heart of the research is an imperative wide spectrum language, WSL. In my talk, I'd like to focus on the design of practical transformation tools, and show results we have obtained. To conclude, I would like to put together some thoughts on what we have learned about building software that can easily and reliably be changed to meet evolving requirements. Some very recent results from a new research project will be included. The talk will be aimed at the general Computer Scientist; by the end of the talk, I hope to convince the audience that formal methods can indeed be used successfully on large-scale heavily maintained software.

Potts Models, Chromatic Polynomials, and All That
Tuesday 3rd August 1999 - Professor Alan Sokal (New York University):
The q-state Potts model is a statistical-mechanical model that generalizes the well-known Ising model. It can be defined on an arbitrary finite graph G, and its partition function is a polynomial that encodes much important information about G (including its chromatic polynomial and its reliability polynomial). The complex zeros of the Potts-model partition function are of interest both to statistical mechanicians (in connection with the Lee-Yang picture of phase transitions) and to combinatorists. I begin by giving an introduction to all these problems. I then sketch two recent (and as yet unpublished) results: (a) Proof of a universal upper bound on the q-plane zeros of the chromatic polynomial (or, more generally, antiferromagnetic Potts-model partition function) in terms of the graph's maximum degree (maximum number of nearest neighbors to any vertex). (b) Construction of a countable family of planar graphs whose chromatic zeros are dense in the whole complex q-plane except possibly for the disc |q-1| < 1. This talk is intended to be understandable to both mathematicians and physicists; no prior knowledge of either graph theory or statistical mechanics is required.