Formal Methods – 2003, Oxford, UK

Citation

Mann, C.J.H. (2004), "Formal Methods – 2003, Oxford, UK", Kybernetes, Vol. 33 No. 7. https://doi.org/10.1108/k.2004.06733gab.006

Formal Methods – 2003, Oxford, UK

The teaching of Formal Methods (FM) at universities worldwide and at other institutions is well established. Now perhaps is the time to reflect on the way in which this has been accomplished and on what has worked well, what has not worked so well, and where particular difficulties lie. This was the theme that Steve Schneider of Royal Holloway, University of London, developed in his invited talk. Professor Schneider presented the opening paper at the “Teaching FM Practice and Experience Workshop” organised by Oxford Brookes University, Oxford, UK, and supported by the British Computer Society-Formal Aspects of Computing Science (BCS-FACS) in December 2003. He described the way in which teaching formal methods has evolved over the past decade at Royal Holloway. These included courses on Applications of FM, the B-Method, Z and CSP.

Delegates from all over the world were then presented with a programme of 17 papers that covered in some detail a whole range of FM teaching practices and an insight into the development of FM topics and courses. There is little doubt that the workshop was unique in its concept and in the manner in which it was organised inasmuch as it allowed delegates to interact in a most productive way. It certainly justified the opening remarks by John Nealon in his official welcome.

It would be invidious to pick out any one of the excellent presentations featured in the programme, but some did provide both fascinating and worthwhile study. Neville Dean (Anglia Polytechnic University) for example, reminded us that our first task in FM courses was to get “students thinking and not to go straight into the Z notation”. This strategy may sound rather obvious, but in fact is so often ignored by academics who are so anxious to teach a programming language. Teaching a student to think is necessary and it is, we were told, not necessary to teach any particular programming language. The importance of getting a feedback from industry was also stressed in many of the papers given.

Dyke Stiles (Utah State University, USA) gave an outline of “Informal methods in a Computer Engineering Curriculam”. He described courses in the use of formal methods in the design of concurrent software systems for postgraduates. It was interesting to note that in the last 4 weeks students worked in pairs on a major project with no lectures. Steve King (York University, UK) delivered a position paper about the assessment of students on FM courses. He produced some new ideas including the notion that students should review specifications and not write them. My own paper “From Z to SPIN in one module” an FM module introduced in the School of Informatics (University of Wales, Bangor, UK) was described. Some of the problems and issues faced, together with student performance and feedback, were also considered. One of these observations concerned the variety of student mathematical backgrounds and a resulting FM course that is broad based and does not tackle the proof or refinement of specifications.

The presented papers and the additional papers were published by our hosts and no doubt would be made available (Teaching Formal Methods, 2003) to those in the cybernetics and systems communities with interests in FM. It was quite apparent to all who attended that in addition to the main workshop theme being thoroughly covered by the presented papers, an insight was also given into the current advances in FM research and development. It may be regarded as simplistic to suggest that the content of any FM course is a function of the R&D, but it was noted from the examples of content and the applications given that there could be no agreed syllabus for presenting FM at almost any of the levels considered. The other important observation has to be that the perceived standard of any FM course has naturally, got to be tailored to the needs of the course attendees whether given in academia or in industry. Teachers of FM courses have to balance their approaches from the superficial to an in-depth one. Not an easy task it would seem particularly with the growing lack of any mathematical background amongst students.

This workshop can be rated as a realistic “state-of-the-art” forum for the teaching of FM.

Oxford Brookes should be congratulated on their organisation of the event and for a programme which contained so many interesting and worthwhile presentations.

C.J.H. Mann

ReferenceTeaching Formal Methods (2003), BCS-FACS, Oxford Brookes University, Oxford, UK, pp. 1-104.