********************************************************************** セッションS5-a チュートリアルテーマ：目で見て分かるモデル検査講師：早水公二氏（フォーマルテック）日時：2011/9/02 14:30〜15:50 参加人数：15名（終了時） ********************************************************************** ・アジェンダ ○自己紹介 ○モデル検査の概要 ○デモ　○モデル権査ツールの紹介および使用例　○例題・今回のゴール　ソフトウェアの仕様書や設計書などを元にして作成するモデル図の概要を説明し、モデル検査によるソースコードの不具合を発見する原理をデモを交えながら解説する。・自己紹介　早水公二　（はやみずこうじ）　１９７０年生まれ　１９９４年　　京都工芸繊維大学　電子情報工学科　卒業　　　　同年　　メルコ・パワー・システムズ（MPS）入社　２００２年〜　産業技術総合研究所でモデル検査技術を習得　２００４年〜　関西電力株式会社様とモデル検査の普及活動を開始　２０１１年〜　株式会社フォーマルテックを設立　　　　　　　　　形式手法(特にモデル検査)の本格的な普及活動を開始・モデル検査とは？　形式手法（数理的技法）の１つである。例としてSMV、SPINなどがある。　形式手法とは、数学・論理学を基盤としたシステムの記述方法や検証方法の総称である。　仕様書やソースコードなどから「モデル」と呼ばれる専用言語に変換する。要求仕様書や基本性質など、モデルが満たすべき性質を検査式（CTL式）で記述する。これらモデルと検査式をモデル検査器によってシステムを全自動で全数探索する。・不具合が見つかる原理　モデルを検査してモデルの不具合を発見すれば、モデルの基（ソースコードや仕様書）にも不具合がある事がわかる。反例とは不具合に至るまでの経路のことを示す。　作業は、モデルの作成と検査式（CTL式）の作成の２つである。しかし仕様書、設計書、ソースコードのモデル化にはコストがかかる。そのためコストに見合う価値があるかどうかを見極める必要がある。・デモ　モーターを利用したデモ　概要：制御盤からボタンの押下状態を入力する。制御盤には加速ボタンと減速ボタンがある。押しているボタンの状態をセンサーが検知し、その状態（オン・オフ・※欠測）を計算機に送信する。加速ボタンがオンで計算機に「加速中」と表示され、減速ボタンがオンのときは「減速中」と表示される。　※欠測とは、センサーがデータを取れなかった、または取得したデータが信用出来ないものの場合を示す。　例：　「加速ボタンを押している間は加速中表示だった（正しい）」　「しかし、加速ボタンを離して減速ボタンを押したのに加速中表示のままだった（正しくは減速中と表示される）」　どこに不具合があるか？　モデル化：ソースコードからモデルを作成する　検査方針：不具合の状態が発生しないはず　検査項目：加速オフで減速オンで表示が加速中となり続けることはないはず　SMV（モデル検査ツール）に上記のモデルを入力すると、検査方針の項目に対して「False」と表示される。つまり不具合が存在することがわかる。　反例を解析すると、「加速押下→加速離す→減速押下」の経路で不具合が発生することがわかる。　この場合「加速離す」瞬間で加速側に欠測が発生し、加速中表示のまま減速を押下することによりデッドロックに陥る。不具合はこの場合に限るため再現がとても難しい。・モデル検査に関する書籍　「モデル検査：基礎から実践まで４日で学べる（初級編）」　「モデル検査：実践のための３つの技法（上級編）」　「SPINモデル検査ー検証モデリング技法」　の３冊の書籍を紹介されました。・企業での普及活動　開発現場では膨大な量の仕様書、ソースコードの検査をする必要があるが、３２ビットのモデル検査器では限界がある。そのため関西電力株式会社からの委託研究開発として６４ビット版モデル検査器を新規に開発し、独自の効率化手法を導入した。　産業技術総合研究所検証クラスター「さつき」（メモリ１TB）を利用して検査の大幅な高速化が確認できる。・モデル検査WEBサービスの紹介　６４ビット版モデル検査器と大容量メモリ搭載の計算機「さつき」を用いていつでも誰でも利用できる Webサービスとして公開されている。　利用方法：　１．ユーザーがモデルを送信する。　２．検証クラスター「さつき」においてモデルを検査する。　３．ユーザーが検査結果を受信する。　メリット：　モデル検査器のインストール不要　ライセンス問題を考える必要がない　大容量メモリ「さつき」を利用できる　いつでもどこからでも手軽にモデル検査ができる　本システムで初公開の６４ビット版モデル検査器を利用できるため状態爆発の回避に有効　無料（関西電力＋産総研による支援）　セキュリティについて：　匿名で利用可能　SSL暗号化での通信　処理は全自動なので人では介さない　モデルと検査結果はご利用後に全て削除・デモ　Webページ「実践！ソフトウェアモデル検査」(http://www.modelcheck.jp/service/index.html) へアクセスし、先ほどと同じモデルを実際に送信してみると、IDとパスワードが発行される。結果は同様に「False」となる。・例題１　タスクの優先度と排他制御のシステム・例題２　状態遷移表の検査・例題３　回路図の検査 ○質疑応答＜質問者１＞ CTLの場合、次の状態を示すものがあるがどれだけ使うことがありますか? ＜回答＞ Xの記号を使うことは殆どありません。 Pertial Order Reduction のオプションを使うべきかもしれないですね。＜質問者２＞様々な状態を扱っているようですが、今までで最大のものはどれくらいの状態を扱ったことがありますか？＜回答＞ SMVで億の１桁くらいならノートPCなどで利用することができるが、今までの最大はデスクトップマシンでの20兆状態位です。