Vicki L. Almstrum, The University of Texas at Austin, USA
C. Neville Dean, Anglia Polytechnic University, UK
"Formal methods" is a collective phrase for a body of techniques that share a mathematical basis. Nancy Leveson (1990) explains that
A broad view of formal methods includes all applications of (primarily) discrete mathematics to software engineering problems. This application usually involves modeling and analysis where the models and analysis procedures are derived from or defined by an underlying mathematically precise foundation.
While the use of formal methods is not yet pervasive in industry, their use is increasing in many areas of both the software and hardware industries. This increase may well be helped by the increasing availability of good software tools. Nevertheless there are still problems in the education and training of a workforce capable of applying formal methods. In the preface to the volume Teaching and Learning Formal Methods, co-editors Dean and Hinchey (1996) state
... the need arises for an appropriately educated and trained workforce that can apply the results of existing and future academic research to the practical problems real-world. This means that graduating engineers, mathematicians and computer scientists must have a sufficient background in the relevant mathematics, as well as hands-on experience in applying formal methods.
Likewise, Johnson, Alexander, and Shiu-Kai (1999) observe
In order to attain the capability to build high confidence systems in significant numbers and at a greater scale, it is essential that a much larger number of students be trained in engineering applications of formal methods.
However, being faced with "formal methods" can raise strong negative reactions among computing students as well as among computing educators. For some, the mathematics involved is intimidating. For others, the learning curve is a huge barrier. Providing instructors and students with improved support in this area would be a positive contribution to the computing field.
Over the last decade there has been a growing interest in the educational aspects of formal methods and many workshops have been arranged. Generally these provide opportunities for formal methods educators to share ideas, but there is a growing feeling that something more concrete is needed for those instructors and curriculum designers who are not formal methodists, and for those formal methodists who are coming to teaching the subject for the first time.
The working group's primary goal will be to build a clear picture of the support that is available in the area of formal methods education, and to provide guidelines for educators who are coming to teaching formal methods for the first time.
Although there is now plenty of materials and software available (for example see http://www.cs.indiana.edu/formal-methods-education/), there seems to be little or no coherent guidance and help on
The FMWG will clearly define each of these aspects and survey the field to summarize the tools and techniques in common use.
Three major goals of the FMWG will be to assist computing educators to:
As part of this, the working group participants will investigate
In preparing the deliverables, the FMWG will survey existing research so that they can describe current knowledge and suggest areas for further investigation. One starting point for investigating this area is The Formal Methods Educational Materials Repository (http://www.cs.indiana.edu/formal-methods-education/), a collection of pointers to course pages, tools, examples, and reading materials for formal methods courses. Although this repository is fairly comprehensive it does not provide much guidance to the newcomer, and indeed may well add to an educator's sense of confusion or of being overwhelmed!
The Formal Methods Working Group will produce two major deliverables. The first will be the report that, if accepted, will be published as part of the December 2000 SIGCSE Bulletin. This report will provide the CS Education community with a static resource on the topic of formal methods. The report may be seen as a "handbook" for educators that will enable them to make effective use of the available materials.
The second deliverable from this WG will be web-based materials from the report, which will provide a dynamic and enduring resource on this topic. The working group will determine the best host for the material; one possibility is the server at UT Austin. The working group will also ensure that these materials are linked into the appropriate points throughout the World Wide Web, including the Formal Methods Educational Materials Repository (http://www.cs.indiana.edu/formal-methods-education/), Jonathan Bowen's formal methods web site (http://archive.comlab.ox.ac.uk/formal-methods.html), and other sites related to formal methods.
The working group will be limited to five to ten participants (including the leaders) who share a common interest in the area of Formal Methods, selected on the basis of their qualifications in the area. Much of the working group's survey work will take place via electronic communication during the spring and early summer, so that the WG participants will arrive in Finland prepared to flesh out and compile the final report. We project that the major efforts toward this preliminary work will begin about May 5, 2000 [a slight delay from the original plan of May 1, 2000].
All working groups will meet at the conference site the day before the conference, throughout the conference and the day after the conference (July 10-14, 2000). We will determine our own meeting schedule. While working group members should be able to participate in many other conference activities, their main commitment during the days of the conference is to the working group.
Intermediate working group results will be presented to all conference attendees at a poster session early in the conference schedule. At the conference conclusion, the working group will submit a polished report. The report will be reviewed and, if accepted, distributed to all conference attendees, published in a SIGCSE Bulletin, and published in the ACM digital library.
We invite applications from individuals with a wide variety of backgrounds in order that we can ensure an appropriate breadth of coverage in the reports. These backgrounds might include education, academic research, industry, software engineers, managers; anyone, in fact, who might have ideas on what and how formal methods should be taught.
The application period has been extended to end on May 2, 2000 (the original date was April 17, 2000). In order to apply as a participant, prepare a proposal with the following information:
Plain text electronic submissions are preferred. This will facilitate sharing of information with working group leader s, who will ultimately determine the membership of their own groups. Send your application to Erkki Sutinen, the Working Group Coordinator, at Erkki.Sutinen@joensuu.fi.
For further details and to express an interest in the Formal Methods Working Group please contact:
- email: almstrum@cs.utexas.edu
- Dept. of Computer Sciences
TAY 2.124 (C0500)
The University of Texas at Austin
Austin, TX 78712- Telephone: +1-512-471-9737 (work)
- Fax: +1-512-471-8885
Both Vicki Almstrum and Neville Dean have been active in the Formal Methods Education community for a number of years. Dr. Dean is author of the textbook The Essence of Discrete Mathematics (1997). He was co-editor of the volume Teaching and Learning Formal Methods (Dean & Hinchey, 1996); Dr. Almstrum was a contributing author to this volume. Dr. Dean has organized Educational Issues sessions at the Z Users' Group Meetings several years running; these sessions provide educators with the opportunity to share issues of formal methods with one another. Dr. Almstrum was the WG coordinator at ITiCSE '97 and a WG leader at ITiCSE '96.
Almstrum, V. L. (1996) Investigating student difficulties with mathematical logic. In Dean and Hinchey (Eds.) Teaching and Learning Formal Methods, London: Academic Press.
Dean, C. N., and M. G. Hinchey (Eds.) (1996) Teaching and Learning Formal Methods. London: Academic Press.
Johnson, S. D., Alexander, W. P. and Shiu-Kai Chin (1999) Report on the 21st Century Engineering Consortium Workshop: a Forum on Formal Methods Education, http://www.cs.indiana.edu/formal-methods-education/xxiec/report.html.
Leveson, N. G. (1990) Guest Editor's Introduction: Formal Methods in SW Engineering, IEEE Transactions on SW Engineering, 16(9), Sept 1990, 929-931.