| Submission Procedure |
|
|
|
||||||||
Curriculum Vitae: Richard Banach received the degree of B.Sc. in Mathematical Physics in 1976 from Birmingham University (UK). This was followed in 1977 by a Diploma in Advanced Studies in Science, and in 1979 by a Ph.D. in Theoretical Physics, both from Manchester University (UK). The field of study for his doctorate was quantum field theory in topologically non-trivial spacetimes. There followed three further years as a researcher in theoretical physics, studying quantum field theory. In 1982 he joined International Computers Limited working on the development of the ICL 3980 mainframe. There, his main areas of responsibility lay at the hardware/software interface: from address translation microcode, through the design and implementation of the global synchronisation primitives for multinode systems, (the ICL 3900 series machines were probably the first commercially available machines featuring a globally cache coherent, physically distributed virtual memory model), and thence to multinode error recovery strategy. In 1986 he rejoined Manchester University, this time in the Computer Science Department, as a lecturer, and since 1986 a senior lecturer. For the next few years he was associated with the Alvey Flagship Project, a large multifaceted collaborative research enterprise, whose objective was the design of a novel system architecture, encompassing parallel hardware, a graph rewriting based computational model, applicative programming models, novel operating system structures, and applications. His work again included the hardware/software interface of the system, but eventually concentrated on the design of the MONSTR language and computational model, which became the definitive programmers' interface for the Flagship machine. MONSTR is a term graph rewriting language which constrains the flexibility of the unrestricted generalised term graph rewriting model of computation, in such a way that direct execution on parallel hardware becomes conceivable, without an excessive loss of expressivity. After Flagship berthed in the late 1980's, his interests become more concerned with the theory of graph rewriting. MONSTR is a language which is expressive enough to use in practice, but whose operational semantics are simple enough to be amenable to rigorous study, and various questions concerning the equivalence of different semantic models for the MONSTR syntax occupied his attention; especially those which enable an implementation to skimp on things like synchronisation and strict adherence to serialisability, without destroying higher level conformance to a rewriting semantics. The applicability of MONSTR for expressing in a natural manner various aspects of novel programming paradigms as they gain popularity, is intermittently the subject of publications. Further issues regarding the semantics of graph rewriting have been of interest. These include the correspondence between the term graph rewriting model and other graph rewriting models, such as the double pushout approach; the categorical semantics of graph rewriting in general, particularly fibration semantics (a particularly elegant abstract diagrammatic semantics has been developed for the double pushout approach); and the possibilities for type inference within graph rewriting formalisms. One aspect of many of these topics that makes them particularly intriguing is the absence of one of the theoretician's favourite tools, structural induction, caused by the presence of cycles within graphs. Other research interests have included: linear logic, particularly the correspondence between proof nets, interaction nets, and conventional graph rewriting formalisms; concurrency theory as expressed in the Pi-calculus, CCS, and its comparison with graph rewriting; and the utility of regular relations within specification disciplines. Formal methods have been a major area of activity for some time, with a focus on the B-Method, and especially as applied to problems described by continuous mathematics, which plays such an important role in real world situations as exemplified by embedded systems. This has obvious repercussions for safety- critical system development. One advance has been the introduction of the notion of retrenchment, which is a liberalisation of refinement, permitting the controlled breaking of the proof obligations of refinement, and permitting the mixing of I/O and state aspects of operations in the passage from the abstract to the concrete model. Retrenchment generally permits more of the informal aspects of engineers' model building to be formally captured. Retrenchment resonates strongly with application builders, who experience the limitations of the familiar refinement technique on a daily basis. It also subsumes many previous attempts to break out of the 'refinement straitjacket' that are to be found in the literature. Most recently, the increasing popularity of real-world systems that contain components that interact with the physical world, so-called cyberphysical systems, has led to a redirection of the existing formal methods interests towards methodologies for the top-down design and development of such systems. In particular, it has led to the development of Hybrid Event-B, an extension of the B-Method for top-down design and development of cyberphysical systems. Dr. Banach regularly acts as a reviewer for work in the formal methods area, and is a Foundation Editor of the Journal of Universal Computer Science.
Main Research Interests:
|
