WIP：面向软件工程专业本科生的TLA+模型检查入门趣味课程
WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
AI总结：
该研究探索将TLA+模型检查等形式化方法融入本科及研究生计算机教育，设计了从入门到进阶的阶梯式课程内容，初步结果显示84%学生反馈积极，为培养掌握形式化方法的软件工程师提供了可行路径。
摘要：
研究背景：本文介绍了我们将形式化方法（重点是用行为时序逻辑（Temporal Logic of Actions, TLA+）编写的模型检查规约）融入计算机科学教育的初步工作，授课对象为本科三/四年级学生及研究生。形式化方法在保障安全关键系统的正确行为方面可发挥关键作用，但在教育和工业场景中仍未得到充分利用。研究目标：我们旨在（1）定性评估计算机科学专业课程中形式化方法的教学现状；（2）构建适合本科中期学习阶段的难度适配的示例；（3）演示如何通过逐步严格的安全性和活性要求来解决接连出现的“失效”问题；（4）建立一个持续评估学生兴趣和相关度的框架。研究方法：课程从数理逻辑复习入手，学生用TLA+编写简单谜题的规则，并使用其内置的模型检查器TLC求解。我们逐步提升难度，过渡到更复杂的动态事件驱动系统（例如微波炉的控制逻辑），让学生学习安全性和活性要求。随后我们通过对有界计数器和缓冲区建模，讲解显式并发、线程安全以及死锁避免相关内容。研究结果：初步发现表明，通过精心的课程设计以及示例和工具的选择，完全有可能激励并培养出精通形式化方法的新一代软件工程师。研究结论：初步教学实践显示，84%的学生在我们的形式化方法课程中获得了积极的学习体验。未来计划包括在本校开展纵向分析，并提议与其他院校合作，探索我们的开源开放获取教学模块的有效性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
