Ebook: Teaching Formal Methods: CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18-19, 2004. Proceedings

“Professional engineers can often be distinguished from other designers by the engineers’ ability to use mathematical models to describe and 1 analyze their products.” This observation by Parnas describes the de facto professional standards in all classical engineering disciplines (civil, mechanical, electrical, etc.). Unf- tunately, it is in sharp contrast with current (industrial) practice in software design, where mathematical models are hardly used at all, even by those who, 2 in Holloway’s words “aspire to be engineers.” The rare exceptions are certain critical applications, where mathematical techniques are used under the general name formal methods. Yet,thesamecharacteristicsthatmakeformalmethodsanecessityincritical applicationsmakethemalsoadvantageousineverydaysoftwaredesignatvarious levels from design e?ciency to software quality. Why, then, is education failing with respect to formal methods? – failing to convince students, academics and practitioners alike that formal methods are truly pragmatic; – failing to overcome a phobia of formality and mathematics; – failing to provide students with the basic skills and understanding required toadoptamoremathematicalandlogicalapproachtosoftwaredevelopment. Until education takes these failings seriously, formal methods will be an obscure byway in software engineering, which in turn will remain severely impoverished as a result.

---

This book constitutes the refereed proceedings of the CoLogNet/FME Symposium on Teaching Formal Methods, TFM 2004, held in Ghent, Belgium in November 2004. The 15 revised full papers presented together with an invited paper and 2 abstracts of invited talks were carefully reviewed and selected from numerous submissions. The papers presented explore the failures and successes of formal methods education, consider how the failures might be resolved, evaluate how to learn from the successes, and attempt promoting cooperative projects to further the teaching and learning and the usage and acceptance of formal methods. Table of Contents Cover Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18-19, 2004, Proceedings ISBN: 3540236112 eISBN: 354030472X Preface Table of Contents A Beginner's Course on Reasoning About Imperative Programs 1 Introduction 2 Previous Courses 3 The Current Course: Reasoning About Programs IV 4 First-Order Logic 5 Reasoning About Imperative Programs 6 Motivation 7 Evaluation 8 Lessons Learnt 9 Conclusion References Designing Algorithms in High School Mathematics 1 Introduction 2 Theoretical Framework 3 Examples 4 Related Work 5 Conclusions References Motivating Study of Formal Methods in the Classroom 1 Introduction 2 Motivating with Examples 3 Discussion References Formal Systems, Not Methods 1 Background 2 Developing the SPM 3 Conclusions References A Practice-Oriented Course on the Principles of Computation, Programming, and System Design and Analysis 1 The Basic Questions and Concepts 2 Algorithms: Computability and Undecidability 3 Principles of Programming Languages 4 High-Level System Design and Analysis References Teaching How to Derive Correct Concurrent Programs from State-Based Specifications and Code Patterns 1 Introduction 2 Teaching Concurrent Programming 3 Notation and Logic Toolkit 4 Deriving Ada 95 Protected Objects 5 Deriving Message Passing Systems with Rendez-Vous 6 Related Work 7 Conclusion References Specification-Driven Design with Eiffel and Agents for Teaching Lightweight Formal Methods 1 Introduction 2 Eiffel, Design-by-Contract, and Agents 3 Specifications and Requirements 4 Teaching Formal Methods with Eiffel 5 Some Observations and Conclusions References Integrating Formal Specification and Software Verification and Validation 1 Introduction 2 Related Work 3 Course Overview 4 Relevant Assessment Tasks 5 Feedback 6 Concluding Remarks References A Sample Graph Solution Distributed Teaching of Formal Methods 1 Introduction 2 Distributed Teaching 3 Formal Methods in Undergraduate Courses 4 Summary References An Undergraduate Course on Protocol Engineering - How to Teach Formal Methods Without Scaring Students 1 Introduction 2 Student Profile 3 Initial Approach 4 Case-Based, Tool-Oriented Approach 5 Benefits of This Approach 6 Conclusion and Future Plans References Linking Paradigms, Semi-formal and Formal Notations 1 Introduction 2 Some Limits and Implicit Assumptions 2.1 Examples of Implicit Assumptions Closed world, unicity of names, closure of the domain. When we were 3 Linking Notations, Techniques, and Paradigms 4 Linking Algebraic and State-Based Specifications 5 Linking Codd Relational n-ary Model, B, and Phasing 6 Conclusion References Teaching Formal Methods in Context 1 Introduction 2 Formal Methods and Software Engineering 3 A Programme of Professional Education 4 Experiences and Results 5 Conclusions References Embedding Formal Development in Software Engineering 1 Background 2 Experience at UNSW 3 Experience 4 Objectives for the Future 5 Conclusion References Advertising Formal Methods and Organizing Their Teaching: Yes, but... 1 Preamble: The Essence of Formal Methods: What Are They? 2 Advertising and Promoting FMs: Yes, but ... 3 So What? Integrating the Teaching of FMs Within Engineering Curricula 4 Conclusions References A Acronyms Retrospect and Prospect of Formal Methods Education in China 1 Introduction 2 The Present Status 3 Comparisons in View of Western and Eastern Culture Differences 4 Suggestions References A Survey of Formal Methods Courses in European Higher Education 1 Introduction 2 Related Work 3 Survey Description 4 Survey Analysis 5 Conclusions and Further Work References A Tentative Body of Knowledge for Formal Methods Author Index