This workshop is organized by the
Formal Methods Europe Subgroup on Education.
- Dines Bjørner (JAIST, Japan)
- Eerke Boiten (University of Kent, UK)
- Raymond Boute (Universiteit Gent, Belgium)
- Andrew Butterfield (Trinity College, Dublin)
- John Fitzgerald (University of Newcastle upon Tyne, UK)
- Randolph Johnson
- Steve King (University of York, UK)
- Peter Lucas
- Michael Mac an Airchinnigh (Trinity College, Dublin)
- Dino Mandrioli (Politecnico di Milano, Italy)
- Andrew Martin (Oxford University, UK)
- José Oliveira (Universidade do Minho, Portugal) -- Convenor
- Kees Pronk (Technische Universiteit Delft, NL)
- Simão Melo de Sousa (Universidade da Beira Interior, Portugal)
- Wolfgang Reisig
(Humboldt-Universität zu Berlin, Germany)
Workshop Co-Chairs
Raymond Boute
Formal Methods Group,
Department of Information Technology (INTEC),
Ghent University,
Ghent (Belgium)
E-mail: boute@intec.UGent.be
José Oliveira
Departamento de Informatica
Universidade do Minho, Braga, Portugal
E-mail: jno@di.uminho.pt
| 9h00 |
- |
Tool Support for Learning Buchi Automata and Linear Temporal Logic, by Yih-Kuen Tsay, Yu-Fang Chen, and Kang-Nien Wu |
| 9h30 |
- |
Supporting Formal Method Teaching with Real-Life Protocols, by Hugo Brakman, Vincent Driessen, Joseph Kavuma, Laura Nij Bijvank and Sander
Vermolen |
| 10h00 |
- |
A Playful Approach to Formal Models, by Katharina Spies, Bernhard Schaetz |
| 10h30 |
- |
COFFEE BREAK |
| 11h00 |
- |
Two courses on VDM++ for Embedded Systems: Learning by Doing, by Peter Gorm Larsen |
| 11h15 |
- |
Comments on several years of teaching of modelling programming language concepts, by J W Coleman, N P Jefferson, and C B Jones |
| 11h30 |
- |
A Graduate Seminar in Tools and Techniques, by Patrick J. Graydon, Elisabeth A. Strunk, M. Anthony Aiello, and John C. Knight |
| 11h45 |
- |
Teaching the Mathematics of Software Design, by Emil Sekerinski |
| 12h00 |
- |
Basic Science for Software Developers, by David Lorge Parnas and Michael Soltys |
| 12h15 |
- |
Introducing Model Checking to Undergraduates, by Abhik Roychoudhury |
| 12h30 |
- |
LUNCH BREAK |
| 14h00 |
- |
Evaluating a Formal Methods Technique via Student Assessed Exercises, by Alastair F. Donaldson and Alice Miller |
| 14h15 |
- |
Enhancing student understanding of formal method through prototyping, by Andreea Barbu and Fabrice Mourlin |
| 14h30 |
- |
From Run-time Analysis to Static Analysis of Java Programs: A Teaching Approach, by Christelle Scharff and Sokharith Sok |
| 14h45 |
- |
The Use of an Electronic Voting System in a FM Course, by Alice Miller and Quintin Cutts |
| 15h00 |
- |
Teaching with the Computerised Package Language, Proof, and Logic (LPL), by Roussanka Loukanova |
| 15h15 |
- |
COFFEE BREAK |
| 15h45 |
- |
FORUM |
| 17h00 |
- |
END OF WORKSHOP |
- Electronic proceedings (1.4Mb PDF)
- Slides
of all presentations
Motivation
Quoting Dines Bjørner:
| |
“Formal Methods Education is currently
facing a ‘trichotomy’.
- On the one hand, industries dealing with the design of complex and critical systems have an increasing need for methods that provide a certain degree of confidence in the result, and are often looking for external assistance in the area of formal methods from consulting companies and academia.
-
On the other hand, a growing number of university staff enjoys the intellectual challenge of research in this area and teaching formal techniques to students.
- On the ‘third hand’, an increasing number of students de-select
formal methods in the curriculum, due to various causes and trends.”
|
One cause of the problem is a general mathphobic trend in society and education.
Another cause is that, intellectually, Information Technology is the victim of its own success. Indeed, the rapid growth creates so many design and implementation tasks that can be done and, more importantly, are being done with negligible educational or scientific background that it is difficult to argue convincingly in favor of formal methods on the basis of immediate everyday necessities. Critical systems, of course, are a notable exception.
These trends are so pervasive that the small minority of FM educators has little hope to curb them in the near future. More effective in the long term is instilling a higher degree of professionalism in the next generation. This requires in particular a directed, positive action towards motivating students.
Theme
This workshop solicits short papers, presentations, demonstrations and evaluations describing sharp classroom or lab experiments which have proved particularly beneficial to the students' understanding and motivation for formal methods.
The emphasis is not on (new) theories or methods but on specific illustrations
and exercises that can be used by colleagues in their own courses, perhaps
applying their own formalisms.
The main goals are:
- to share knowledge and experience on the practicalities of teaching and learning formal methods;
- to build a collection of interesting cases, examples, assignments and projects that FM teachers can use in educational activities.
Format
The workshop will be a forum-like event, with short presentations, demos and
informal discussion slots. After the workshop, if the evaluation committee decides
that there is a sufficient number of high-quality submissions, an agreement will be
sought with Springer Lecture Notes in Computer Science about publishing a special volume, and authors will be
invited to submit their contribution for refereeing.
Call for Contributions
This workshop solicits papers, presentations, demonstrations and evaluations describing such material in detail and how it has been beneficial to the students' understanding and motivation.
The emphasis should not be primarily on new theories or methods but on
specific illustrations and exercises that can be used by colleagues in
their own courses, perhaps applying their own formalisms.
The central problem(s) should be clearly stated and a typical solution outline
provided (using the author's preferred method), accompanied by a discussion
of what educational aspect is meant to be enhanced. Contributors should
motivate their techniques with a discussion of the desired knowledge and
skill outcomes of the examples/case studies or projects, and a frank appraisal
of their effectiveness, insofar as such an appraisal is meaningful and instructive,
which we expect to be the case for most topics.
Papers should be kept short (maximum 6 pages). They should be prepared preferably in LaTeX, and a pdf-file should be sent to jno@di.uminho.pt. Submitted papers will be evaluated by the Subgroup on Education.
Timings
Submission deadline: Friday, June 9, 2006
Acceptance notification: Saturday, July 1, 2006
The organization will produce a web-based resource of output from the workshop housed under http://www.fmeurope.org. Contributors willing to allow their teaching materials to be made publicly available for the community are invited to send source files, links or tools and other information that would be suitable for such an on-line repository, which the organization will keep alive on a wiki-like basis.
The collected material will form the start of a compendium of examples, cases, assignments and projects, according to the following (rough) categorization.
- Examples are shorter items, ranging in length from a single observation to over a full page. An example is aimed at clarifying a single aspect where the essence is captured in a somewhat condensed form, with minimal clutter from side-issues.
- Cases are taken from situations encountered in practice, where the problems may appear in various forms: from immediately appealing (and hence motivating) but not very challenging to subtly hidden and requiring major research. Side-issues and secondary problems may be included to clarify the setting or to illustrate the need for abstraction.
- Assignments and projects correspond to examples and cases respectively, but the difference is that they are elaborated by the students rather than the instructors.
The repository is expected to evolve in at least 3 dimensions:
- new items are added in their original form as time proceeds;
- existing items are reworked in various formalisms;
- experience in teaching is reported.
Every one or two years, people who submit the most suitable contributions will
be invited to join forces for combining their work into a "laboratory notebook".
Any further suggestions are welcome.
|
Proceedings 