Experiential Learning of Runtime Monitoring Using Pachinko

在航空与自主飞行的高端领域，工程师们面临着一个艰巨的挑战：如何确保复杂的机器在实时运行时表现正常。这些系统通常由庞大的团队构建，其复杂程度之高，使得在投入使用前无法进行完美的检查。为了解决这个问题，专家们使用了一种称为“运行时监控”（runtime monitoring）的技术。想象一下，有一个专门的安全卫士时刻注视着机器的数据流，不断检查数字和事件是否符合一套严格的规则。如果机器开始偏离安全路径，这个卫士就会发出警报或采取纠正措施，以防止灾难发生。虽然这一概念对于保障飞机和无人机的安全至关重要，但向学生教授这一概念却非常困难。相关的场景通常涉及规模巨大且抽象的系统，难以在课堂上进行可视化，这使得学习者很难理解为什么需要如此严格的规则。

巴纳德学院（Barnard College）和哥伦比亚大学（Columbia University）的一个教育团队找到了一种方法，通过将课堂变成一个关于日本游戏“柏青哥”（Pachinko）的工作坊，使这一抽象概念变得具体可感。在他们最近的研究中，他们设计了一项课程作业，让学生构建受计算机系统实时监控的互动式柏青哥盘。其目标不仅是建造一个游戏，更是教导学生如何编写“形式化规范”（formal specifications）——即精确的逻辑规则，告诉计算机应该观察什么以及如何做出反应。通过使用一个钢珠会在数千个钉子间不可预测地弹跳的物理游戏，研究人员创造了一个让安全监控的需求显得迫切且真实的场景。学生们学习了如何为一个小型的计算机芯片编程，使其观察球的运动、检测模式并根据这些模式触发声音或电机动作，从而有效地将一个游戏转化成了一堂关于安全关键型软件的课程。

该项目围绕着一个装有数百个黄铜钉并设有钢珠滚动路径的木制盘面展开。在这个盘面的底部，有一个小型电子设备，它充当了游戏的“大脑”及其安全卫士。该设备配备了传感器，可以检测球何时通过特定的通道，从而跨越铜箔上的微小间隙。研究人员设置了系统，使该中央设备在其内部处理器上同时运行两个独立的任务。一个处理器负责处理读取传感器和与其他设备通信的物理工作，而第二个处理器则运行“监控器”。这个监控器是一段软件，它不断地根据学生编写的一套规则来检查球的运动流。

学生们以小组为单位，负责使用一种专门用于描述基于时间事件的语言来编写这些规则。他们必须决定哪些球的运动模式会触发响应。例如，一名学生可能会写下一条规则，规定：“如果一个球连续两次通过这个特定通道，则向电机发送信号。”当监控器检测到规则被满足时，它会立即向盘面上的其他设备发送无线消息。这些设备控制着步进电机，可以物理移动游戏的部件，或者触发灯光和声音。整个过程是在实时中进行的，创造了一个动态循环，即游戏的行为会根据学生定义的逻辑规则而改变。

研究人员发现，学生们在编写这些控制游戏行为的形式化规则方面表现得非常出色。学生遇到的主要困难并非来自逻辑或代码，而是来自游戏的物理构建。连接传感器、布设电机线路以及确保不同电子板之间的无线通信顺畅运行，被证明是最具挑战性的部分。这一结果本身也是一次宝贵的教训。在现实世界中，运行时监控常用于硬件与软件必须完美协作的复杂系统中。通过在布线和物理设置上的挣扎，学生们体验到了专业工程师在构建无人机或飞机安全系统时所面临的同类集成挑战。

学生在使用提供的工具时也存在一些技术限制。他们用于编写规则的软件不支持某些复杂的基于时间的运算，例如统计长时间内的总球数。为了解决这个问题，学生们必须发挥创造力，利用主处理器来计数，然后将这些总量发送给监控器。虽然这并不是教授这些特定概念的最理想方式，但它表明学生仍然能够运用形式化逻辑来解决问题。研究人员指出，他们正在致力于改进软件，以便未来能够处理这些更复杂的运算。

该项目的成功表明，教授先进的安全概念并不一定需要抽象的模拟或大规模的工业装置。通过将课程植根于一个物理的、互动的游戏中，教育者使运行时监控的需求变得清晰且引人入胜。该项目的材料相对廉价，每个盘面的成本约为七十五美元，且其设置旨在易于在其他课堂中复制。该系统具有灵活性，传感器的数量和电机的数量都可以更改，允许该作业根据不同的班级规模或创意目标进行调整。最终，该项目证明，只要给学生一个具体、动手实践的方式去观察这些规则如何运作，他们就能掌握形式化验证和实时安全监控的原理。