Formal Methods Teaching : Third International Workshop and Tutorial, FMTea 2019, Held As Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings

This book constitutes the refereed proceedings of the Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 2019. The 14 full papers presented together with 3 abstract papers were carefully reviewed and selected from 22 submissions. The papers are organized in topical sections named: Tutorial lectures; Teaching Program Verification; Teaching Program Development; and Effective Teaching Techniques. -- Provided by publisher Preface 6 Organization 8 Invited/Tutorial Lectures 9 Is Formal Methods Really Essential? 10 pseuCo.com 11 Efficient Online Homologation to Prepare Students for Formal Methods Courses 12 Contents 13 Tutorial Lectures 15 Logic, Algebra, and Geometry at the Foundation of Computer Science 16 1 Introduction 16 2 Algebra and Logic 17 2.1 Boolean Algebra 17 2.2 Deductive Logic 19 2.3 Spatio-Temporal Logic 21 3 Sequential Composition 23 3.1 Hoare Triples 24 3.2 Verification Rules for Sequential Composition 24 3.3 Milner Transition 25 4 Concurrent Composition 25 4.1 Interchange 26 4.2 Basic Principle of Concurrent Programming 26 4.3 Unifying Theories of Concurrency 27 5 Related Work 29 6 Conclusion 30 References 31 Teaching Program Verification 34 Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists 35 1 Introduction 35 2 Why Is It Difficult to Teach Formal Methods at ISAE-SUPAERO? 36 2.1 The ISAE-SUPAERO Engineering Program 36 2.2 The Challenges 37 2.3 Why Teaching Formal Methods at ISAE-SUPAERO? 38 3 Introducing Formal Methods in 17 h 38 3.1 Deductive Verification with Frama-C and SPARK 39 3.2 A Top-Down Approach with Frama-C 39 3.3 A Bottom-Up Approach with SPARK 41 3.4 Comparison of Both Approaches 43 4 The SPARK by Example Experiment: Learning from Examples 43 4.1 What Is SPARK by Example? 43 4.2 A Corpus of Proved Algorithms 44 4.3 Lessons Learnt 45 5 Conclusion 46 References 47 Using Krakatoa for Teaching Formal Verification of Java Programs 49 1 Introduction 49 2 Context of Our Experience 50 3 Study of Different Alternatives 52 4 Some Examples of Formal Verification with Krakatoa 55 4.1 Lectures in the Computer Classroom 55 4.2 Exercises in the Computer Classroom 60 4.3 The Exam 61 5 Results of the Experience 61 6 Conclusions and Further Work 62 References 62 Teaching Deductive Verification in Why3 to Undergraduate Students 64 1 Introduction 64 2 Background on Why3 66 3 Learning to Write Precise Specifications 67 3.1 Testing of Specifications 68 3.2 Testing Larger Specifications 70 3.3 Loop Invariants 71 4 Towards More Complex Specifications 73 4.1 Type Invariants 74 4.2 Ghost Code 74 5 Proving Recursive Programs 75 6 Conclusion 77 References 78 Teaching Program Development 79 Teaching Formal Methods to Future Engineers 80 1 Introduction 80 2 ENSIIE 81 3 Software Engineering and Security Track 82 4 Formal Methods for Reliable Systems (MFDLS) 83 5 Mechanized Formal Proof and Semantics (PROG1) 86 6 Static Analysis and Deductive Verification (PROG2) 88 7 Conclusion 89 References 90 The Computational Relevance of Formal Logic Through Formal Proofs 92 1 Introduction 92 2 Logical Deduction Frameworks 94 3 Logical Deduction versus Proof Commands 96 4 Inductive Proofs Versus Recursive Algorithms 98 5 Related Work and Conclusions 104 References 106 Teaching Formal Methods: From Software in the Small to Software in the Large 108 1 Introduction 108 2 Content of the Subject 110 2.1 Model Checking/SPIN 111 2.2 Alloy 112 2.3 UML/OCL 113 3 Methodology 114 3.1 Model Checking 115 3.2 Alloy 116 3.3 OCL 117 4 Assessment and Results 117 5 Conclusions 119 References 120 On Teaching Applied Formal Methods in Aerospace Engineering 122 1 Introduction 122 2 Approach 125 3 Tools and Techniques 128 4 Research Paper Presentations 130 4.1 Professor's Presentation Evaluation Form 131 4.2 Student's Presentation Evaluation Form 132 5 Student Projects 132 5.1 Initial Project Plan: Statement of Work 132 5.2 Progress Report and Preliminary Results 133 5.3 Final Report and Presentation to the Class 134 5.4 Example Student Projects 134 6 Conclusions and Outlook 137 References 139 Effective Teaching Techniques 143 Teaching Concurrency with the Disappearing Formal Method 144 1 Introduction 144 2 State Diagrams for Sequential Programming 146 3 State Diagrams for Concurrent Programming 150 4 Course Notes and Delivery 155 5 Conclusions 156 References 157 Teaching Discrete Mathematics to Computer Science Students 159 1 Introduction 159 2 Background 161 3 Games and Winning Strategies 163 4 Labelled Transition Systems 164 4.1 Introducing LTSs with Puzzles 165 4.2 The Man-Wolf-Goat-Cabbage Riddle 165 4.3 The Water Jugs Riddle 166 5 Verification via Games 167 5.1 The Formal Definition of Equivalence 168 5.2 The Copy-Cat Game 168 5.3 Relating Winning Strategies to Equivalence 169 5.4 Determining Who Has the Winning Strategy 170 6 Conclusion 172 References 173 Principled and Pragmatic Specification of Programming Languages 174 1 Introduction 174 2 The Course 176 3 How We Teach SOS 178 4 The eSOS Interpreter 183 5 The eSOS Concrete Syntax 185 6 Connecting Parsers to eSOS 186 7 Student Response and Conclusions 188 References 188 Managing Heterogeneity and Bridging the Gap in Teaching Formal Methods 190 1 Introduction 190 2 The Study Programmes and Their History in Short 191 2.1 Computer Science 191 2.2 Business Information Systems 192 2.3 2-Area Programme 192 2.4 International Programme 192 3 Managing Heterogeneity 192 3.1 Teaching Approaches for Managing Heterogeneity 193 4 Bridging the Gap 196 4.1 Students 197 4.2 Teaching Schemes for Bridging the Gap 199 5 Quantitative Data and Evaluation 202 5.1 Managing Heterogeneity 202 5.2 Bridging the Gap 202 6 Conclusion 203 References 204 Teaching Introductory Formal Methods and Discrete Mathematics to Software Engineers: Reflections on a Modelling-Focussed Approach 205 1 Introduction 205 2 Related Work 207 3 Context 207 3.1 The Software Engineering Programme 208 3.2 Courses and Assignments 208 3.3 The Software Engineering Mathematics Course 209 4 The Approach 210 4.1 The Motivation for Change 210 4.2 A Change in Emphasis 211 4.3 Benefits and Challenges 211 4.4 An Example 211 5 Indicative Results 213 5.1 Student Performance 213 5.2 Feedback 215 6 Conclusions 216 References 217 Teaching Formal Methods: Lessons Learnt from Using Event-B 221 1 Introduction 221 2 Our Students 223 3 The Survey at Carnegie Mellon University 224 3.1 Recommendations 227 3.2 Implementation of Recommendations at Innopolis University 228 4 The Survey at Innopolis University 229 4.1 Student's Feedback 230 4.2 Related Aspects 233 5 Related Work 234 6 Conclusion 234 References 235 You Already Used Formal Methods but Did Not Know It 237 1 Introduction 237 2 My Experience with Teaching the IM 238 2.1 You Already Used Formal Methods 238 2.2 The Need for Formal Methods and in Particular for the IM 240 2.3 A Parallel: How to Write a Biography 241 2.4 The Use of Computational Logics for Reasoning 242 2.5 The Basics of Functional Programming 243 2.6 The Wonders of Mathematical Induction 243 2.7 The Formal Protocol Definition 245 2.8 The Main Functions 247 2.9 The Basic Interaction with the Theorem Prover 248 2.10 Proof Attempts 249 3 General Lessons Learned and Conclusions 251 References 251 Author Index 253 Front Matter ....Pages i-xvi Front Matter ....Pages 1-1 Logic, Algebra, and Geometry at the Foundation of Computer Science (Tony Hoare, Alexandra Mendes, João F. Ferreira)....Pages 3-20 Front Matter ....Pages 21-21 Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists (Léo Creuse, Claire Dross, Christophe Garion, Jérôme Hugues, Joffrey Huguet)....Pages 23-36 Using Krakatoa for Teaching Formal Verification of Java Programs (Jose Divasón, Ana Romero)....Pages 37-51 Teaching Deductive Verification in Why3 to Undergraduate Students (Sandrine Blazy)....Pages 52-66 Front Matter ....Pages 67-67 Teaching Formal Methods to Future Engineers (Catherine Dubois, Virgile Prevosto, Guillaume Burel)....Pages 69-80 The Computational Relevance of Formal Logic Through Formal Proofs (Ariane A. Almeida, Ana Cristina Rocha-Oliveira, Thiago M. Ferreira Ramos, Flávio L. C. de Moura, Mauricio Ayala-Rincón)....Pages 81-96 Teaching Formal Methods: From Software in the Small to Software in the Large (María-del-Mar Gallardo, Laura Panizo)....Pages 97-110 On Teaching Applied Formal Methods in Aerospace Engineering (Kristin Yvonne Rozier)....Pages 111-131 Front Matter ....Pages 133-133 Teaching Concurrency with the Disappearing Formal Method (Emil Sekerinski)....Pages 135-149 Teaching Discrete Mathematics to Computer Science Students (Faron Moller, Liam O’Reilly)....Pages 150-164 Principled and Pragmatic Specification of Programming Languages (Adrian Johnstone, Elizabeth Scott)....Pages 165-180 Managing Heterogeneity and Bridging the Gap in Teaching Formal Methods (Pamela Fleischmann, Mitja Kulczynski, Dirk Nowotka, Thomas Wilke)....Pages 181-195 Teaching Introductory Formal Methods and Discrete Mathematics to Software Engineers: Reflections on a Modelling-Focussed Approach (Andrew Simpson)....Pages 196-211 Teaching Formal Methods: Lessons Learnt from Using Event-B (Néstor Cataño)....Pages 212-227 You Already Used Formal Methods but Did Not Know It (Giampaolo Bella)....Pages 228-243 Back Matter ....Pages 245-245 This book constitutes the refereed proceedings of the Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 2019. The 14 full papers presented together with 3 abstract papers were carefully reviewed and selected from 22 submissions. The papers are organized in topical sections named: Tutorial lectures; Teaching Program Verification; Teaching Program Development; and Effective Teaching Techniques. -- Prové de l'editor