Document Type

Conference Proceeding

Publication Date

10-14-2024

Publication Title

IEEE

Pages

1-5

Publisher Name

Figshare

Abstract

Background: In this Innovative Practice Work in Progress, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), into computer science education, targeting undergraduate juniors/seniors and graduate students. Many safety-critical systems and services crucially depend on correct and reliable behavior. Formal methods can play a key role in ensuring correct and safe system behavior, yet remain underutilized in educational and industry contexts.

Aims: We aim to (1) qualitatively assess the state of formal methods in computer science programs, (2) construct level-appropriate examples that could be included midway into one's undergraduate studies, (3) demonstrate how to address successive ``failures'' through progressively stringent safety and liveness requirements, and (4) establish an ongoing framework for assessing interest and relevance among students.

Methods: We detail our pedagogical strategy for embedding TLA+ into an intermediate course on formal methods at our institution. After starting with a refresher on mathematical logic, students specify the rules of simple puzzles in TLA+ and use its included model checker (known as TLC) to find a solution. We gradually escalate to more complex, dynamic, event-driven systems, such as the control logic of a microwave oven, where students will study safety and liveness requirements. We subsequently discuss explicit concurrency, along with thread safety and deadlock avoidance, by modeling bounded counters and buffers.

Results: Our initial findings suggest that through careful curricular design and choice of examples and tools, it is possible to inspire and cultivate a new generation of software engineers proficient in formal methods.

Conclutions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. Our future plans include a longitudinal analysis within our own institution and proposals to partner with other institutions to explore the effectiveness of our open-source and open-access modules.

Comments

Author Posting © IEEE, 2024. This is the author's version of the work. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. The definitive version of this work was published at 2024 IEEE Frontiers in Education Conference (FIE) Proceedings at https://doi.ieeecomputersociety.org/10.1109/FIE61694.2024.10893422

Creative Commons License

Creative Commons Attribution 4.0 International License
This work is licensed under a Creative Commons Attribution 4.0 International License.

Download

Share

COinS