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