报告人： Richard Banach 博士
School of Computer Science, University of Manchester, Manchester M13 9PL, UK.
报告题目：The Mondex Purse: Requirements and Retrenchments
报告时间：2010年5月10日下午2：30
报告地点： 数计学院5-107 （原106改为107）
参加人员：计算机学科全体教师和在新校区研究生
Abstract：This talk gives a broad overview of retrenchment, as it has been applied to Mondex. The Mondex Electronic Purse is a development which is now very thoroughly understood from a verification perspective. Verification has to presuppose that all requirements issues are settled definitively one way or another, since it is committed to a particular formal system model, or models. However, there is often room for a diversity of views in modeling specific system details, and some such issues are reviewed in the context of Mondex. Topics examined include: the treatment of atomicity in Mondex, and its generalisation to cover arbitrary isolated protocols; replays and denial of service attacks; sequence numbers and their boundedness; exception logs and their boundedness; non-injective log-clear codes; balance enquiries inthe midst of a protocol run. Retrenchment, a liberalisation of conventional model based refinement, has a distinctive role to play in all of these.
报告人简介：
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 ultinode 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. 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 mplementation 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 become a major new area of activity, with some 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. A recent 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.Since 1996 Dr. Banach has been a senior lecturer. He is a Foundation Editor of the Journal of Universal Computer Science."},"user":{"isNewRecord":true,"name":"系统管理员
