Paul's Research Page (Formal Methods)

I intended to develop a site that offers a personal treatment of this mathematical approach to developing software. When last I was investigating this area in mid 1998, there weren't many Formal Methods pages independent of academic centres and companies, so I wanted to fill some of the gap.

However, my career has since moved away from this area towards Internet Development. So these pages are unlikely to be developed much further - unless someone discovers something of outstanding originality in my thesis ;-)

Nevertheless, you may like to at least find out some basic information.


Research Interests

In October 1997, I was awarded a Ph.D. in The Use of Formal Methods for Safety-critical Systems. You can download a copy of the thesis from here. For the thesis, my external examiner was Prof. Ken Turner and the internal examiner was Mr. Phil Molyneux.

I undertook the research in the School of Computer Science and Electronic Systems at Kingston University. I did my brain-storming in the Sopwith Building which also houses other Schools in the Faculty of Technology. My Director of studies (main supervisor) was Dr. Katherine Norrie.

The research had a practical focus owing to informal collaboration with the Department of Medical Informatics at the Royal Free Hospital School of Medicine in North London. There emerged the Medical Software Engineering Group which sought to apply some formal techniques to the study of embedded medical systems. Hence, one of my other supervisors was Mr. Phil Curran.

I was particularly interested in making use of the insights of systems safety engineering for integrating formal methods in safety-critical software development. I produced a survey cum argument for the use of formal methods in safety-critical systems, which was written in LaTeX and converted to html using Latex2html.

I had access to the log files and noticed that this report had many visitors, many of whom would read more than just the odd page. Looking around, I found that information about formal methods is generally fragmented. Hence I developed a proposal for the EU to make a large coherent reference base - now archived here. It was my first attempt at an EU funding application.


And the future ... ??

I recall that as I was nearing the end of my studies, Tony Hoare, a leading light in the field, delivered a paper entitled, "How did software get so reliable without proof?" Now looking back at the turn of the Millennium, we may wonder at how there were so few reported incidents of Y2K bugs causing havoc?

There is a lot more to software production than formal procedures and mathematics ..!


- Paul Trafford Paul's home page

Last modified: 15 September 2000