Teaching Formal Methods

1. Front Matter

   PDF

2. Abstraction and Modelling: A Complementary Partnership

   • Jeffrey Kramer

   Pages 1-1

3. Teaching Formal Methods for the Unconquered Territory

   • Nestor Catano, Camilo Rueda

   Pages 2-19

4. Teaching Formal Methods Based on Rewriting Logic and Maude

   • Peter Csaba Ölveczky

   Pages 20-38

5. Which Mathematics for the Information Society?

   • João F. Ferreira, Alexandra Mendes, Roland Backhouse, Luís S. Barbosa

   Pages 39-56

6. What Top-Level Software Engineers Tackle after Learning Formal Methods: Experiences from the Top SE Project

   • Fuyuki Ishikawa, Kenji Taguchi, Nobukazu Yoshioka, Shinichi Honiden

   Pages 57-71

7. Chief Chefs of Z to Alloy: Using a Kitchen Example to Teach Alloy with Z

   • Sureyya Tarkan, Vibha Sazawal

   Pages 72-91

8. Teaching Program Specification and Verification Using JML and ESC/Java2

   • Erik Poll

   Pages 92-104

9. How to Explain Mistakes

   • Stefan Hallerstede, Michael Leuschel

   Pages 105-124

10. Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification

    • Wolfgang Ahrendt, Richard Bubel, Reiner Hähnle

    Pages 125-143

11. On Teaching Formal Methods: Behavior Models and Code Analysis

    • Jan Kofroň, Pavel Parízek, Ondřej Šerý

    Pages 144-157

12. Teaching Concurrency: Theory in Practice

    • Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiří Srba

    Pages 158-175

13. Back Matter

    PDF

This volume contains the proceedings of TFM2009, the Second International FME Conference on Teaching Formal Methods, organized by the Subgroup of Education of the Formal Methods Europe (FME) association. The conference took place as part of the ?rst Formal Methods Week (FMWeek), held in Ei- hoven, The Netherlands, in November 2009. TFM2009 was a one-day forum in which to explore the successes and fa- ures of formal method (FM) education, and to promote cooperative projects to further educationand training in FMs. The organizersgatheredlecturers,tea- ers,andindustrialpartnersto discusstheir experience,presenttheir pedagogical methodologies, and explore best practices. Interest in FM teaching is growing. TFM2009 followed in a series of events on teaching FMs which includes two BCS-FACS TFM workshops (Oxford in 2003, and London in 2006), the TFM2004 conference (Ghent, 2004, with p- ceedings published as Springer LNCS Volume 3294), the FM-Ed 2006 workshop (Hamilton, co-located with FM2006), FORMED (Budapest, at ETAPS2008), and FMET2008 (Kitakyushu, co-located with ICFEM2008). FMs have an important role to play in the development of complex c- puting systems—a role acknowledged in industrial standards such as IEC61508 and ISO/IEC15408, and in the increasing use of precise modelling notations, semantic markup languages, and model-driven techniques. There is a growing need for software engineers who can work e?ectively with simple, mathematical abstractions, and with practical notions of inference and proof.

• Debugging
• Maude
• algorithms design
• calculus
• code analysis
• imformation society
• logic
• modeling
• program debugging
• program specification
• program testing
• program verification
• rewriting logic
• semantic markup language
• verification

• Computing Laboratory, Oxford University, Oxford, UK

  Jeremy Gibbons

• Departamento de Informática, Universidade do Minho, Braga, Portugal

  José Nuno Oliveira

Policies and ethics