********************************************************************** ワーク S2-de テーマ：80分で分かるモデル検証講師：小川清（名古屋市工業研究所）日時：2009/08/28 9:00-10:20 参加人数：16名 ********************************************************************** 9:20開始【講義を始める前に】・USBメモリをI使う。VMWPlayer ISOイメージのファイル・GRUBをインストールする・本(4日で学ぶモデル検査)を買う【対象者】・前提知識 →日本語できる →C言語（プログラミング言語）が出来る →PC操作・仕事 →システムの設計・開発・検証の技術者 →事業の管理者 →学生【講義】 ■□■□■□■□■□■□■□■□■□■□■□■□■□■□ ★モデル検査を好きになって帰ってもらいたい講師様の意見 ■□■□■□■□■□■□■□■□■□■□■□■□■□■□ ○モデル検査の必要性 →試験しやすいような設計・従来の形式手法の困難性 →背景となる理論のわかりやすい説明がない →インストール方法がわからない →どういうモデルをつくればいいかわからない ○本の紹介・4日で学ぶモデル検査 →KNOPPIX:CD起動Linux →Xspin：X-Windowsで動作するSPIN(simple promela inter preter) →4日分の実例 →インストールしなくても利用できる →理論の説明より前に操作の説明 →入力と出力が画面で切り替えられる →自習可能な十分なモデル例 ○SPINについて →裏でGCCが動くので、Cプログラマにとって安心感がある →技術者にとって並列捜査のプログラムを書くのが良くわからない →LTL（時相論理）式を入れると、成立か不成立か確かめ可能 ○本紹介 →コンピュータプロトコルの設計法 →ファイル転送をpromelaで記述 →promelaの記述のある初期の本 ○SPINでできること →モデル検査による不具合の検出（デッドロック、ライブロック、制約違反、不必要なコード検出） ○SPINを利用する課題 →利用困難 →導入が難しい（システム導入の方法がわからないなど） →モデルの記述（なにを書けば良いのか不明確） →LTL式の記述（何を検査したらよいのか不明確） ○Promela →Promela: protocol meta language →SPIN: Simple Promela interpreter →C言語、C++, Java, C#, Pascal, Modula-2, Adaなどのプログラミング言語 →四則演算（加減乗除）、論理演算(not, and, or), 判断(等価、大、小） ○論理回路設計の検証 →並列動作が前提なので、並列動作の記述に抵抗がない →状態遷移の検証から実施すると、状態遷移記述の大事さも分かる ○論理演算子・論理結合子・論理命題演算子説明 ○実施環境の構築 →CDブート（GRUBを導入） →VMWareでの起動(VMWare Playerの導入) →Co-linux+X →cygwin+X ○構築の流れ・CドライブにKNOPPIXというフォルダ作成・Windows起動状態で、CDのinstall2win.batを実行・Grubをインストール（boot\grub\）・環境変数を設定・KNOPPIXというフォルダを作成し、KNOPPIXのコピー・再起動でGRUBを選択してKNOPPIXを起動・VMWarePlayerをダブルクリック・ショートカット作成＆ライセンス認証・起動ファイル指定 ○Xspinの操作手順・[K]メニューのxspin選択・Promelaを入力（ファイルから読み込みも可）・Run - SyntaxCheck（文法誤りがあるとエラーが出る）・Run ?LTL property manager （FromulaにLTL式を書く、ファイルから読み込みも可）・Generate （ボタンを押すと未定義論理変数の一覧が出てくる→式（値）を記述する）・Run ?Verification →Valid 仮説が検証された →Not valid ・反例が存在する・Run Guided simulation ・Single step または RUN ・Xspinの操作手順 →資料参考（パワポ）・本日は例を２つやる・１つ作業したらい、一回すべて消して新しいファイルをつくる・上書きは警告なしでされるので注意・ソースコード例・”；”は並列動作を表す＆最後の行は”；”がいらない →それ以外はふつうのCと同じ・【本日の例題】 ① →ワイン店について →論理回路を設計し、設計したものがしっかり動くかができるかどうか →一度論理回路をONにしたら、OFFにできる状態になるまでOFFにならない →ワイン店についての設計の説明（pptファイルp56,57） →ホワイトボードに状態遷移図説明（デジカメで撮影）・8-1-p →LUNのシンタックスチェックをしてみる →LUNのLTLプロパティマネージャを立ち上げLTLも走る →Validだとうれしくない・8-2のモデルの8番目や2番目のLTLモデルnot valid ＃演習は講義者のPCで実際やってみながら行っている＃各個人のPCで演習＃主に教材はspinというフォルダ内＃６番目のLTL間違ってる→エラーでる＃VMCはやってない＃コンパイラもOSも少しづつ検証してどこに要因があるのかを出す 9：45 システムインストールができてない人3名ほど（USBがまわりきれていないため）【課題】どういうLTL式を立てれば、モデルの必要十分な検証できることになるか記述したLTL式が正しいかどうか確認することが困難【相談事項】・状態番号の打ち方 →0からｎの十進数 or 4ビット２進数・遷移の表現・自動生成【Q&A】 Q：8-1-pファイルはどこにあるのか？ Q：どれをみながら打ち込むのか？ Q：７から０はどういくのか？（状態遷移図の話） !recpatron Q：LTLの式に制約をつけないとvaridになるが、その制約はどのように定義しているのか？ A：なかなか難しい・システマティックにやるのは難しい Q：Spinでモデル化したときもしくはLTLのときに間違いやすいか？ A：→Spinでのモデル化のときのほうが間違いやすい →仕様書の部分からしっかりできてないことが現状なため Q：状態遷移図について（細合さん）状態遷移図を階層的に書いて、個別の状態遷移図を個々に作成すれば自動でやってくれるのに、人が考えて設計するのはなぜ？ A：階層的に書いて、一番下の階層について検証する状態遷移で理想論式を立てると検証できるというのが本の内容だが、どの用に検証するか記述してなかったので、今回はPlomeraを採用した・使用したSWは必ずSWEST後に消去してください（小川さん）・ただしVMWPlayerを継続して使用する場合、VMWPlayerのライセンスは各自で取ってください（小川さん） ○4日間で学ぶモデル検査・操作説明→理論→演習・インストール簡単 ○非同期回路の設計・並列動作前提のたえ、並列動作に抵抗がない ○コンピュータプロトコルの設計法・内容にSPINが書いてあることがあまり知られていない ■まとめ ○Xspinを用いた体験型のワーク・Xspinの環境構築・ワイン店の課題をXspinを用いて個人で取り組む以上。