Seminars

A Refinement Based Approach to Hybrid Systems: Basics and Event-B Design PDF (1) & PDF (2)
Richard Banach– Professor, School of Computer Science, University of Manchester

09/14/2012, 2pm, GHC 6501

Abstract

We outline some of the issues that arise in pursuing a refinement based approach to the hybrid and cyber-physical systems being developed today, supporting the view that a combination of refinement and retrenchment techniques gives the best coverage. We outline a semantic framework for hybrid systems. We go on to consider how to integrate the hybrid ideas into the Event-B framework, which was intially conceived for discrete transitions alone. Development in Event-B is predominantly controlled by the generic verification conditions that are instantiated for each individual development, and we show how these can be extended to cover the new hybrid features.

Biography

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.

http://www.cs.man.ac.uk/~banach/