Experiential Learning of Runtime Monitoring Using Pachinko

航空業界や自律飛行という極めて高い信頼性が求められる世界において、エンジニアたちは困難な課題に直面しています。それは、複雑な機械がリアルタイムで稼働している際に、それらが正しく動作することをどのように保証するかという問題です。これらのシステムは多くの場合、多くの人々によって構築されており、スイッチを入れる前に完璧にチェックすることは不可能です。この問題を解決するために、専門家は「ランタイム・モニタリング（実行時監視）」と呼ばれる手法を用いています。これは、機械のデータストリームを見守る専任の警備員を想像すると分かりやすいでしょう。その警備員は、数値やイベントが厳格なルールと一致しているかどうかを常にチェックしています。もし機械が安全な経路から逸脱し始めたら、この警備員は惨事が起こる前にアラームを鳴らすか、是正措置を講じます。この概念は航空機やドローンの安全を守るために不可欠ですが、学生に教えるのは容易ではありません。シナリオの多くは、巨大で抽象的なシステムを扱っており、教室の中で可視化することが難しいため、学習者がなぜそのような厳格なルールが必要なのかを理解するのが難しいのです。

バーナード・カレッジとコロンビア大学の教育者チームは、教室を日本の「パチンコ」のワークショップに変えることで、この抽象的な概念を具体的なものにする方法を見出しました。彼らの最近の研究では、学生がインタラクティブなパチンコ台を製作し、それをコンピュータシステムがリアルタイムで監視するという課題を設計しました。その目的は、単にゲームを作ることではなく、コンピュータに対して「何を監視し、どのように反応すべきか」を正確に指示する論理的なルール、すなわち「形式仕様（formal specifications）」を書く方法を教えることでした。何千もの釘に鋼鉄の玉が無作為に跳ね返る物理的なゲームを用いることで、研究者たちは、安全モニターの必要性が即時的かつ現実的に感じられるシナリオを作り出しました。学生たちは、小さなコンピュータチップをプログラミングして、玉を監視し、パターンを検出し、そのパターンに基づいて音やモーターの動きを誘発させる方法を学び、実質的にゲームを安全クリティカルなソフトウェアのレッスンへと変えたのです。

プロジェクトの中心となるのは、数百本の真鍮の釘が打ち込まれた木製の盤と、鋼鉄の玉が転がり落ちる経路です。この盤の底部には、ゲームの「脳」であり「安全ガード」でもある小さな電子デバイスが設置されています。このデバイスには、特定のチャンネルを玉が通過した際、銅テープのわずかな隙間を橋渡しすることを検知できるセンサーが備わっています。研究者たちは、この中央のデバイスが内部プロセッサ上で2つの異なるタスクを同時に実行するように設定しました。一方のプロセッサは、センサーの読み取りや他のデバイスとの通信といった物理的な作業を担当し、もう一方のプロセッサは「モニター」を実行します。このモニターは、学生が書いた一連のルールに従って、玉の動きのストリームを絶えずチェックするソフトウェアです。

学生たちは小グループに分かれ、時間の経過に伴うイベントを記述するために設計された特殊な言語を用いて、これらのルールを書く課題を与えられました。彼らは、どのような玉の動きのパターンが反応を引き起こすかを決定しなければなりませんでした。例えば、「もしボールが特定のチャンネルを2回連続で通過したら、モーターに信号を送る」といったルールを記述することができます。モニターがルールを満たしたことを検知すると、即座に盤上の他のデバイスへ無線メッセージを送信します。これらのデバイスはステッピングモーターを制御しており、ゲームの部品を物理的に動かしたり、ライトや音を鳴らしたりします。このプロセス全体はリアルタイムで行われ、学生が定義した論理的なルールに基づいてゲームの挙動が変化するという、ダイナミックなループを生み出します。

研究の結果、学生たちはゲームの挙動を制御するためのこれらの形式的なルールを書くことに、驚くほど成功していることが分かりました。学生が直面した主な困難は、論理やコードそのものではなく、ゲームの物理的な構築にありました。センサーの接続、モーターの配線、そして異なる電子基板間の無線通信をスムーズに機能させることは、最も困難な部分でした。この結果自体も、貴重な教訓となりました。現実の世界において、ランタイム・モニタリングは、ハードウェアとソフトウェアが完璧に連携して動作する必要がある複雑なシステムで使用されることが多いからです。配線や物理的なセットアップに苦労することで、学生たちはプロのエンジニアがドローンや航空機用の安全システムを構築する際に直面する、まさにその種の統合の課題を体験したのです。

提供されたツールには、学生が達成できる技術的な限界もありました。ルールを書くために使用したソフトウェアは、長期間にわたる玉の総数をカウントするといった、特定の複雑な時間ベースの操作をサポートしていませんでした。これを回避するために、学生たちは創造力を発揮し、メインプロセッサを使って玉をカウントし、その合計値をモニターに送るという方法を取りました。これは特定の概念を教えるための理想的な方法ではありませんでしたが、学生たちが問題を解決するために形式論理の観点から思考できることを示しました。研究者たちは、将来的にこれらのより複雑な操作を処理できるように、ソフトウェアを改善していく予定であると述べています。

このプロジェクトの成功は、高度な安全概念を教えるために、抽象的なシミュレーションや大規模な産業用セットアップは必ずしも必要ではないことを示唆しています。レッスンを物理的でインタラクティブなゲームに結びつけることで、教育者たちはランタイム・モニタリングの必要性を明確かつ魅力的なものにしました。プロジェクトの教材は比較的安価で、1台あたり約75ドルであり、セットアップは他の教室でも簡単に再現できるように設計されています。システムは柔軟であり、センサーやモーターの数を変更できるため、クラスの規模や創造的な目標に合わせて課題を適応させることが可能です。最終的に、このプロジェクトは、ルールが実際に機能する様子を具体的かつ実践的な方法で提示すれば、学生は形式検証やリアルタイムの安全監視の原則を理解できるということを証明しました。