引导千禧一代学习形式化方法

本文总结了我们在全球多所大学向计算机科学（CS）与软件工程（SE）学生教授形式化方法（FM）课程的经验，包括葡萄牙马德拉大学（UMa）、哥伦比亚哈维里亚那教皇大学（PUJ）和洛斯安第斯大学（Uniandes）、美国卡内基梅隆大学（CMU）以及俄罗斯联邦 Innopolis 大学（INNO）。我们报告了过去 10 至 15 年间向千禧一代本科与研究生讲授 FM 所面临的挑战，并描述了我们如何应对这些挑战。基于经验，我们给出了千禧一代的特征刻画，并展示该刻画如何影响了我们在课程结构与内容方面的决策。我们展示了这些决策如何反映在 MSS（软件系统模型）课程的当前结构中，该课程目前作为 INNO 提供的 MSIT-SE（信息技术硕士——软件工程）项目的一部分运行。我们在学生中开展了两项调查，第一项在 CMU，第二项在 INNO，用于记录并论证我们的决策。第一项调查关于选择 Event-B 作为数学形式体系，第二项关于课堂内基于 Event-B 开展软件项目的学生团队组织方式。