------------------

Research interests

------------------

I am an honorary member of the Verification and Testing Group at Sheffield.

My personal research interests are:

Asynchronous Hardware: I use CCS to specify asynchronous hardware designs and its CWB support tool to show equivalence and prove consequences of specifications using process logics. I have worked with the Amulet group at Manchester University off and on formalising the design of AMULET1, their 2-phase asynchronous version of ARM6. Together with Ken Stevens at ECE Utah, I am now looking at facts and figures on 2-phase pipelines, ditto on 4-phasepipelines, and 2- and 4-phase variants of TK (short for trinket - a cheap, shoddy, worthless amulet, according to Webster's, but hey, what do they know). See also bm, delta, xx, ken, ed.

Simulation: From 1968 through 1973, I was lucky enough to work with the late, great, inspiring and always encouraging Ole-Johan Dahl, Bjorn Myhrhaug and Kristen Nygaard at the Norwegian Computing Center, Oslo. On leaving Norway in 1973, I designed and implemented a OO discrete event simulation extension to Simula called Demos, whose inspiration was Jean Vaucher's GPSSS. The associated text Demos - a system for discrete event modelling on Simula is now out of print, but for those interested, here are postscript and pdf versions of the text. Of late, I have been working with Chris Tofts applying the techniques of process algebra to simulation models and showed how to test models for deadlock, livelock, safety and liveness properties. Chris, now at HP Labs, has produced a new system extending this work. Full details of demos2k can be found here .

[My home page]