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

TL;DR

The paper addresses the underutilization of formal methods in CS education by proposing a TLA+-driven model-checking curriculum for undergraduates and graduates. It presents a microwaves-oven running example and a structured progression from unit testing to safety and liveness properties, validated through TLC-based verification and iterative refinement with invariants and fairness. Key contributions include a curricular design aligned to SE knowledge areas, concrete exemplars, and preliminary evaluation showing strong student engagement (84% positive) and learning gains. The work emphasizes open-source, reproducible materials (GitHub + CI) to enable broader adoption and collaboration across institutions.

Abstract

Background: In this paper, 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. Formal methods can play a key role in ensuring correct behavior of safety-critical systems, 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: 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. Conclusions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. 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.

Figures (7)

• Figure 1: The microwave oven is an engaging and comprehensible, yet non-trivial, example of a safety-critical embedded system worthy of student attention in a Formal Methods course. This figure illustrates how we model two critical requirements: (1) To prevent radiation exposure, the appliance must not run with the door open, and (2) To prevent overheating while radiating, it must eventually turn off (per the TLA+leads to operator $\leadsto$).
• Figure 2: Valid initial states and top-level specification for the microwave oven: Initially, the microwave is not radiating, there is no time remaining, and the door is either open or closed. Subsequently, the model can repeatedly perform any available action, as indicated by the temporal operator "always" ($\Box$).
• Figure 3: Tick action for decrementing the timer, defined as a conjunction of preconditions, effects, and postconditions, where $v'$ refers to a variable's value in the next state following the action. According to the preconditions, this action is enabled only when the oven is radiating and there is nonzero time remaining. Its effect is to decrement the remaining time; when the remaining time reaches zero, its additional effect is to shut off radiation.
• Figure 4: Scenario for normal operation: The microwave is initially radiating with the door closed and one second of time remaining. When the internal timer ticks, the remaining time goes to zero, and the oven stops radiating.
• Figure 5: Scenario leading to an unsafe condition: The microwave is initially stopped with the door open and several seconds of time remaining. When the user presses the start button, the microwave emits harmful radiation.