セミナーの内容

線形時相論理 (Linear Temporal Logic, LTL) にもとづくモデル検査ツールを自分で実装してみようというセミナーです。実装することで仕組みを深く理解できます。自分の好きな言語で作った自分専用のツールというのは愛着のわくものですよね。いろいろと拡張したり、他のツールと組み合わせたりして楽しめます。

モデル検査ツールというのは、プログラムの性質を自動的に検査するツールです。プログラムというのは動くものです。つまり、時間的に変化するものなので、多くの場合、調べたい性質も時間に関係するものになります。

時間に関する性質を表現するために拡張された論理の1つに時相論理というものがあります。よく知られている命題論理に加えて、時間に関する演算子をもっており、これを使って時間に関係するプログラムの性質を表すことができます。

このセミナーで作るモデル検査ツールは、状態遷移モデルとして表したプログラムと、時相論理で表した調べたい性質を入力すると、プログラムが性質を満たしているかどうかを自動的に検査してくれるものです（※1）。検査の結果、満たさないケースがあればレポートしてくれます。それを分析することで、プログラムの誤りを知ることができます。

※1 正確には、時相論理式を外部サービスでオートマトンに変換して、それを入力します。

セミナーは2部構成になっています。第1部では、まずモデル検査の仕組みを説明し、リファレンス実装による設計・実装の方法について解説します。次にモデル検査の実行例を紹介します。第2部では参加者のみなさんに設計・実装をしていただきます。疑問な点を質問したり設計についての相談したりしながら進める形となります。

プログラム

第1部 モデル検査解説

1. モデル検査の概要
2. 計算木・パス・原子命題・ラベリング関数・語
3. 線形時相論理 LTL
4. Büchi オートマトン
5. LTL モデル検査のアルゴリズム
6. リファレンス実装の解説
7. テスト
8. 例：排他制御
9. 公平性
10. 例：通信システム

※ 知っている人への注：LTL 式を Büchi オートマトンに変換する部分は、既存のサービスを利用します。処理全体の中での位置づけは説明しますが、アルゴリズムの解説は行いません。

第2部 モデル検査器の設計と実装

各自、モデル検査ツールを好きな言語で実装します。

講師について

株式会社PRINCIPIA 代表取締役 初谷 久史

プロセス代数 CSP に基づいた検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「モデル検査特論」講師

セミナー参加の前提条件

前提知識

• 高校で習う程度の論理の知識（かつ、または、～でない）
• アルゴリズムの知識：グラフの探索（幅優先探索、深さ優先探索）
• データ構造の知識：ハッシュ表，キュー

デッドロック発見器のセミナーを受けていなくても理解できる構成です。しかし、デッドロック発見器（共有変数またはメッセージ通信による並行合成器）を持っていれば、組み合わせてより面白い検査ができます。

必要なもの

• 使用するプログラミング言語の開発環境（リファレンス実装を動かすためには OCaml の開発環境が必要です）
• Graphviz （dot コマンド）：状態遷移グラフを可視化するために使用します．

Zoom URL

CONNPASS のメッセージにてお知らせします。

配布物

スライド資料（PDF)とリファレンス実装のソースコード（OCaml）を CONNPASS のメッセージにて送付します．

プログラムの大きさの目安

モデル検査器のコードの大きさは、OCaml のリファレンス実装で約270行程度です。

注意事項

• 講師が知らないプログラミング言語については対処が限られます．
• 配布資料の公開は禁止です．

参考書

• ソフトウェア科学基礎

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください．