WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+

Document Type

Conference Proceeding

Publication Date

10-14-2024

Publication Title

IEEE Frontiers in Education

Publisher Name

IEEE

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.

Creative Commons License

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

Link to Full Text

Share

COinS