形式手法特論：作って学ぶモデル検査の理論と実装 by チェシャ猫

ただツールを使うだけの形式手法から、自作する形式手法へ。本セッションでは Go 言語でモデル検査器を実装する流れを紹介しながら、その内部的な仕組みを学びます。

形式手法は計算機システムを何らかの数学的な対象によって記述し、その性質について理論的な保証を得る手法の総称です。通常の単体テストと比較すると記述コストは高くなりますが、その代わりに保証できる内容は数学的な裏付けに基づいており、テストケースの抜けや漏れが発生しません。そのため、分散システムなどの複雑な挙動を設計する場合や、医療・航空宇宙など極めて高い信頼性が求められる場合、言い換えれば高い記述コストを支払っても十分にペイする分野において威力を発揮します。

特に、本セッションで扱う形式手法はモデル検査と呼ばれるものです。形式手法には大きく分けて定理証明とモデル検査の二つの分野がありますが、検査時に人の手が必要な定理証明に対して、モデル検査では基本的に全自動で実行することができます。システムの挙動を Kripke モデルと呼ばれるある種のグラフ構造に変換し、その上で探索を行うのがモデル検査器の基本的な動作原理です。Kripke モデルのノードは可能世界と呼ばれ、モデル検査器は「常に〇〇が成り立つ」「いつかは必ず〇〇が成り立つ」といった時間的な広がりを持った仕様を検査します。それを扱う我々は、さしずめ可能世界を渡り歩く時間旅行者といったところでしょうか。

本セッションでは、講演者が技術書典 16 で頒布した同人誌『モデル検査器をつくる』をベースにして、実際に動作するモデル検査器をスクラッチから実装する流れを紹介します。既存のツールを使用するモデル検査のチュートリアルは巷に多数ありますが、単にユーザとしてツールを使用するだけでは、その背後にある理論や動作原理は見えません。今回は単に「ツールを動かしてみた」で終わらないよう、自作を通してその内部のアルゴリズムまで突っ込んで解説したいと思います。実装言語としては親しみやすさの点で Go を採用しましたが、このセッションを聞いた方が各自の好きな言語で自作を始めることも可能です。

受講にあたって形式手法に関する予備知識は要求しません。また、複雑なシステムの設計や謎の挙動で苦しんだ経験がある人はより楽しめるはずです。さあ、君もその手でモデル検査器を作ろう。