卒論キックオフ 2006/07/25 上田研並列班 1G03R217-5 八鍬 豊
これまでにやったこと モデル検査についての勉強 モデル検査ツールの実践
モデル検査とは システムが正しく動くかどうかを検証する方法の一つ。 数理的技法（形式技法）に分類される。 システムの挙動を計算機の上で模倣し、あらゆる場合をしらみつぶしに調べて検証する。
モデル検査の手順 システムを状態遷移系として表現する。 システムに要求する性質を時相論理式で記述する。 状態遷移系が論理式を満たすかどうかを検査する。
状態遷移系 状態 システムの各瞬間の様子。 遷移関係 状態が次の瞬間にどの状態に変化するか。
状態遷移図
検査する性質 安全性 「悪いことは決して起こらない」 活性 「良いことはそのうち起こる」
時相論理 モデル検査では、時間的な概念を含んだ性質も検査する必要がある。 時相論理とは、そのような時間的な概念を記しやすい論理のこと。 LTL (Linear Temporal Logic) CTL (Computation Tree Logic) etc.
LTLの様相記号 GP FP P UQ XP どの時点でもP が成り立つ。 いずれP が成り立つ。 いずれQ が成り立ち、それまでP が成り立ち続ける。 XP 次の時点でP が成り立つ。
使用したモデル検査ツール Xspin NuSMV
XSpin Spinはコマンドラインアプリケーション。 Xspinは、SpinにGUIを付加したもの。 検査したいシステムをプロセスとして記述。 分散型システムの検証に適している。 Promelaという言語で記述する。 C言語に似ている？
NuSMV NuSMVはコマンドラインアプリケーション。 各状態に現れる変数の挙動を、一元的に制御。 LTLだけでなく、CTLも使用可。 電子回路のようなシステムの検査に適している。 LTLだけでなく、CTLも使用可。
解いた問題 窓辺の花 ウサギとオオカミ
窓辺の花（設定） 窓辺に8個の花が一列に並んでいる。 花は一日単位で開閉する。 花が開くか閉じるかは、その花のご近所の、前日の様子による。 ある花のご近所とは、その花と、その花に隣接する花のこと。
窓辺の花（設定） 前日ご近所で開いていた花の数が 0個の場合、閉じている。 1個の場合、開いている。 2個の場合、開いているか、閉じているかのどちらか。 3個の場合、閉じている。
窓辺の花（問題） 左端の花だけが開いている日があったとして、それ以降、8個の花全てが開く日はあるか？ 答えはデモで。
ウサギとオオカミ（設定） ある川の川岸に、ウサギが3羽、オオカミが3匹、船が一艘。 船の定員は2。ウサギかオオカミのどちらかが操縦しないと動かない。 オオカミがウサギよりも多い状況になると、オオカミはウサギを食べてしまう。
ウサギとオオカミ（問題） 船を使って、ウサギとオオカミ全員が安全に対岸へ渡る手順はあるか？ 答えはデモで。
思ったこと 日本語の資料が少ない。 ツールの性能の良し悪しが分からない。 日本には検証分野が浸透していない？ 現時点では比較対象が少ない。 そもそもツールが使いこなせてない。
どうするべきか 検証分野を学びたい人が、どのツールを使っていいか分からない状況は困る。 様々なツールの特性を明らかにする必要がある。 ツールの性能比較もできればなお良い。
XspinとNuSMVの比較 実行時間 ソースコードの長さ
実行時間 窓辺の花 XSpin : 約0.06sec NuSMV : 約0.04sec ウサギとオオカミ NuSMV : 約0.36sec
ソースコードの長さ 窓辺の花 ウサギとオオカミ XSpin : 47行 NuSMV : 107行 XSpin : 58行
卒論テーマの予定 モデル検査ツールの比較・評価 既存のモデル検査ツールの改良 新たなモデル検査ツールの作製
これからやっていくこと モデル検査の理論の勉強。 モデル検査についての論文を読む。 モデル検査ツールの実践・比較・評価。 ソフトウェア検証にも手を出すかも？
参考文献 「4日で学ぶモデル検査 初級編」 Spin - Formal Verification NuSMV home page 「4日で学ぶモデル検査 初級編」 産業技術総合研究所システム検証研究センター 著 Spin - Formal Verification http://spinroot.com/ NuSMV home page http://nusmv.irst.itc.it/