******************************************************* セッションs2-a/s3-a チュートリアル  テーマ:組み込みソフト技術者のための形式手法入門 講師 篠崎孝一(関西電力)    早水公二(メルコ・パワー・システムズ)    野中哲(トゥルーロジック)    藤倉俊幸(イーソル) コーディネータ 山崎成仁(デンソー) 参加人数:90名程度 ******************************************************** 講師:藤倉 みなさんおはようございます. 形式手法というといろいろありますが,私が使っているのはLTSAというツールです. 形式手法とは数学的な手法によって検証を行うものです. 今は主にこの三つ(定理証明,充足器,モデル検査器)が検証で使われている. 一つ目は現場では使えない. 2つめ以降はボタン一発系. LSI技術と同じなのになぜソフト開発に使えないか.  ソフトは柔軟性がある.  数字の決め打ちは好まれない.  アプリケーションもバラエティに富んでいる.  LSIは一回失敗すると痛い目にあうので形式手法がよい. SATソルバSMPソルバは真理値表を入れてそれを満足するかどうかを判断する. 定理証明は無限大などを扱えるが難しい. モデル検査では状態数は数百万. LSIをやっている人たちはこれを使っている. ○一定感覚で温度測定し,温度が上がり過ぎないように管理する例 この二つのプログラムは同じかどうか.  ・前回測定温度が200℃以上で,その次は200℃未満,だったら安全  ・2回連続して200℃以上だったら危険 論理式に変換してSATソルバに入力すると同じになるので等しい. 定理証明系ではPとQで表して,"PならばQ" は, "Pでないまたは,Q" と同じ.こんな形で客観的に証明できる. 定理証明はよりタイトに客観的に証明していく. ○仕様書の形式化 一番簡単なのは命題論理をつかって書く. 仕様書が与えられたときに命題論理を使う. または時相論理というものも使う. ○モデル検査と検査ツール 現状以下のようなものがある.  LTSA,FDR2,SPIN,NuSMV ○ボールの取り出し方の例 取り出し方の組み合わせは順列組み合わせ. 仕様書では論理式で書けるものがある. モデル検査ツールにはいろいろあるがLTSAは20万程度の状態を扱う. 変数を扱えないので状態数が増えるという欠点もある. LTSAというツールはフリーのツールでダウンロードできる. ○モデルの説明 それぞれのモデルを合成できる. 合成できるだけでなく動きを抽出できる. 例えば,鍵をかけたりはずしたりできるか. lock unlockだけの部分を取り出すことができる. 他にも,入力/出力だけを調べたいとき ログに対応する部分だけを抽出するといった使い方もできる. また,タスク設計などにも使える. 9:42 ○スレッド設計の説明 LTSAによる設計,検証 3つのタスクに分割し、元と比べて差があると検出できる. この例では仕様と異なる動作をしてしまうことがわかる. タスクの実行順序が変わってしまう. 原因は同期機構ができていないから. そこで,コードを変更するとまた別の反例がでてくる. まだ仕様どおりの動きができていない. このように行っていくとどこに同期コードを入れなければいけないかわかってくる. 同期コードを入れていくとだんだん複雑になっていく. 最初の分割が悪いという場合もある. 9:49 ○制御システムの例 いろいろなタスク分割があるが,並列なものが動くときにも使える. 形式手法とどうやって組み合わせていくか. ○関数呼び出しの検証 全体をやると大変なので,見たいポイントを絞り,且つ漏れが無いようにする. 定理証明的なものでなくSATソルバ的なアプローチ 非決定性を決定性に. ○まとめ モデル検査とSATソルバ,これらをどうやって組み合わせていくか, どういう手法をどのように組み合わせるべきかはアプリケーション次第. これからさらにこれらのツールが使えるようになっていくと思われる. 質問  Q. LTSAでは設計の妥当性はLTLによって書けるのか.  A. SPIN等と同様にLTLによって書ける.    Q. 変数とかは出てこないがプロパティを指定してその動きをはみだしていないか,    ほかのひとがみてわかるかどうか.  A. 最近はUML等を使う.まずシーケンス図を理解しないといけない.    モデル検査のモデルをつくるのははまりやすいので,    極力人間がやらずに自動化できるとよい.    9:59 講師:野中 タオベアーズの野中です. 今日のお話はモデル検査ツール御三家の中のSPINというツールの説明をします. SPINとは処理系でPromelaというのが記述言語. もともとは電話交換機の検証に使うため. 2001年にACM Softwareアワード受賞  実用向けのソフトの賞 SPINはもともとコマンドラインベース  その上にGUIなどが充実 特徴は並列処理マルチスレッドの検証が得意という点. また,モデル検査ツールはハードウェア設計が発祥だが SPINはソフトウェア専用のツールである. ○歴史の説明  内部アルゴリズムの発展  現存しているCのコードからモデルを抽出するという動き  2005年以降はマルチコアのCPUのサポート  複数の計算機を検証するとういのが最近の動向 ○プラットフォームの説明 基本的にはコマンドラインが使えれば使用できる. ○SPINの動作モード ・シミュレーションモード  Promelaで書いたものをインタプリタで実行しランダムテストするモード ・検証モード  あらゆる状態遷移を生成 ○処理の流れ  図を使って説明.  Promelaと論理式(今日は説明なし)を使って検証.  モデルの中にアサーションを入れて検証する.  ソースコードが生成され,それをCコンパイラにかけて実行. 10:07 ○Promelaの説明 この三つのオブジェクトを抑えればいい.  ・プロセス お互いに通信する  ・ローカル変数 グローバル  ・チャネル  プロセスのインスタンス化をするための構文はproc_type Hello worldの説明 avtiveを書くと実際にオブジェクトが生成されて実行される. ○データオブジェクトの説明  文字列浮動小数点はない.   シンプルにする 変数としての文字列形は無い.  データ型の宣言の説明  本当にプログラミング言語の記述に似ていますね.    ○チャネルの説明  プロセス間通信のためにつかわれる.  記述方法の説明  ランデブは後で説明する.  イメージの説明(スライド)  具体的な構文の説明  Cという名前のチャンネルを宣言.   10こまでイント型のデータを保持できる.   !マークが送信 モデル検査屋さんの癖   文と文の区切りにセミコロン   受信側はC?   77を送って表示される 10:14 ○制御構造の説明 if文の説明 繰り替えしの説明 ○言語(モデル)のコンセプト この4つぐらいを抑えておく.  ・有限の状態  ・モデル検査とはモデルの取れる状態をすべてコンピュータで作っていく   →有限で無いと不可能  ・変数も有限  ・モデルは閉じている    手元の資料には無いスライドで説明    目的の装置のモデルはユーザインタフェース,センサ,外界からのイベントがあるが,    検証時にはこういったものも全てモデルとして作る必要がある.    全て外側にあるものもモデルとして記述. ○非同期的な実行  モデルの中にプロセスを記述.  並列に実行されるが,どういうタイミングで切り替わるかツールが自動で切り替え.  スケジューリングのタイミングはわからない.  アトミックに行うための指定方法はある. ○非決定性  普通の言語には無い特徴  ガード 一つでも真のガードがあれば実行.  全部falseならブロックされる.  ガードが二つ以上真になった場合,モデルを書いた人はどれが実行できるか制御できない.  SPINが実行してくれる.  たとえばaがどっちになるかわからない.  内部的には乱数によって決まる.  両方の条件でどうなるか調べてくれる.  役に立つ例   ・いつ消えるかわからないパケットを探る.   ・ときどきハードウェアのエラーが起きる.   ○実行可能性  すべてのブロックには実行されるか条件が成立するまでとまるという書き方ができる.  例の説明   xの値による動作の説明 xが3になるまでとまる.   Cのコードとの比較  チャネルに関して   送信側 キューがいっぱいならブロック   受信側 来るまでブロック ○ランデブー  長さ0のチャネル  送信にいくとブロック  受信がいくと何か送信するまでブロック.  このような形でプロセスの同期ができる. ○モデルの中で検証したい性質をどう書くか  assertを挿入する.  assertの中がfalseなら報告してくれる. SPINは内部的には状態ベクトルによって管理  すべてのグローバル変数の値  すべてのプロセスの状態   ローカル変数の値   プログラムカウンタの値  あらゆる状態を内部的に生成 10:27 ○デモの紹介 JSPIN:SPINのうえにIDEのような環境をかぶせたもの.  二つのプロセスが共有変数をアクセスしたらどうなるか.  promelaのソースコードの説明  13行目で10回回ったかどうかを確認してfinishedをインクリメント.  グローバル変数のnをローカルに読み込みインクリメントして書き戻し.   アトミックじゃない   両方が読み込むと正しくインクリメントできない   正しくやると20になるはず  まずインタプリタで実行(ランダム)  n=18,n=15  検証モードで実行.  25行目にnは2よりも大きいというassert ヒットしない.  任意の状態でプロセスが切り替わると全体の状態を13万999生成されていてエラーが一つ見つかる.  アサーションに引っかかったのはどういう状態かトレースが取れる.  このような形で全ての状態を調べてエラーを報告してくれる. ○火星探査機マーズパスファインダの例  プロセスがデッドロック状態になってプロセスがリセットされ,  データが遅れなくなった状態を書いたもの.  ミューテックスを使って同期する二つのプロセス.  何回かランダムで実行するとタイムアウトが発生(デッドロックが発生).  ランダムなシミュレーションでは何回かやってみてたまたま見つかった.  verifyでは必ずエラーを見つけてくれる.  ランダムなシミュレーションでは確率的にしか見つからないものが必ず見つかる. ○XSPINの(SPINのGUIツール)のデモ  パケットの消失を調べるプロトコルのモデル  デーモンプロセスがレシーバが受け取ったものを読み捨てる.   パケットの消失をモデル化したもの   インタープリタで実行   XSPINはメッセージシーケンスチャートを出してくれる.    通信チャネルでどういったデータが送られたかを出してくれる.  右側のグラフィックの部分で通常は2つのプロセスの間で通信しているが,  ときどきデーモンがパケットを食べているのがわかる. 10:45 ○まとめ 並列処理はすごく難しい.  共有資源を安全操作するのは難しい. 状態爆発を防ぐためにいかにシンプルにするか  問題の本質に関係ないところはアトミックに書く. 情報の入手先,参考図書,セミナーの紹介 10:50 質問  Q. ツールは状態数を最適化してくれるのか.  A. 状態数を最適化する内部アルゴリズムは発展している.    Q. 状態の上限はどれくらいか.  A. すこし覚えていないが,10の何上位.    SPINの本家では何十台のPCを使って1週間動かしたという話もある. 11:06 2コマ目を始めます. 講師:篠崎 SMVについて話そうかと思いましたが、 実践のためのガイドを行いたいと思います. モデル検査は2001年ぐらいから使われはじめ, 実際にやってみたらうまくいった. たとえば,新規ソフト開発でやってみたら割込みのところでバグが見つかったなど. しかし,まだまだ使い勝手が悪い,実践的に使うためのノウハウが無い. 実践的に使うためのノウハウが無いなどの課題も. ホームページ(http://www.modelcheck.jp/)の紹介 ○なぜモデル検査なのか 一般的な答え  普段使いこなす中では数学的な前提知識はいらない.  自動化できる.  ある検査項目をいれたときにどういう反例があるか表示してくれて,  それを見れば人間が判断できる. ○事例の説明 踏み切りの例  実は社内でソフトウェア工学を知らない人(上司とか上の人)向けに書いたものです.  まず列車の動きをモデル化   状態遷移図  もう一つのサブシステムとして制御装置 遮断機など  簡単に3つのサブシステムに書いたもの(遮断機,制御装置,列車)  普段はそれぞれのサブシステムについて考えるが,この三つを組み合わせたときに  どうなるかを調べたい.  3桁の数字で状態を表現  不具合の状態は全部の組み合わせの中のどこかにある.  初期状態から,この状態に行くのかどうか.  不具合の状態から初期状態に戻ることができれば,  逆に初期状態からこの状態に遷移することがわかる.  不具合状態にいくパスがわかる.  事例でわかったこと.   ・人間の思い込みによる見落としがちな不具合を検出できる.   ・部分モデルを作るだけでいい.    全体を作らなくても部分を作るだけツールがやってくれる.   ・テストデータが要らない.   ・反例が出てくるのでどういう不具合があるか人間が判断. 11:18 2008年 まだ実践知識が足りない. 座学はできたがどうやって現場に持ち込むか. できるだけ経験者に聞く,やっている他の人とやる. ソフトウェア一般の不具合 システム固有の不具合  対象システムに対する知識が必要.  モデルをしっかり考えないといけない. ハードルは高いのか  ある分野に対象を絞れば自動化はできるのではないか. ○実際にやる上での大きな問題  □作業時間    何回も検査と手直しをやる.  □モデル検査の効果    モデル検査をやることでどの程度テストを減らせるのか.    バグ一個でどれくらい重いのかわからない.   ☆効果はわからないのでコストを減らす方向に.  □関係者の説得   会社の中で説明して,作業の時間を得るのが難しい.    ・なぜ正しいのか.    ・モデル検査器の動作は誰が保障するのか.    ・直感的に理解できない.    ・導入効果のデータ  質問1〜3は技術論に見えるが,経営的観点から  実務者向けの説得だけではだめ.  上司のためのミニ教育が必要  背景知識の無い人を納得させるだけの説明  直感的なイメージをつかんでもらう  動くほうしか見ない,まずいほうは見ない.  早く見つけるためには,人間の視点からではなく,機械で行う.  自動検査を強調  □実践経験の不足   どんな問題があるか.   検査項目をどうやって決めるか.    やっている人から情報を得る.  □SPIN,SMVは研究用で使い勝手が悪い.   モデル検査用言語での記述は手間なのでフロー図から生成できるように.   時相論理式の記述が難しい.    よく使うものはライブラリ化するなどの対応   GUIを使うと絵で見て「見える」ということが大きい.  これまでは言語が読める人しかわからない.  情報共有ができない.  そこでGUIを使うことでみんなが見て判断できる.  関係者みんながチェックして直したり,直さなかったりしてシステムを仕上げることができる. ○無駄,失敗を防ぐためのノウハウ モデル検査導入の課題は言語,時論理式によるものだけではなかった. 検査対象の選定  まず,モデル検査に適しているのか.   状態遷移系でみることに意味があるのか.   何を検査するのか.   出てきた結果を社内のみんなが認めてくれるか.  仕様書を対象とするのか設計書を対象とするのか.  細かく分割して検証  実際に動かしてバグによる不具合が出ても,たまにしかおきない場合は,  そこにかかわる部分を抽出して,検査することで効率的に行える.  発注側と開発者の間で評価が異なる.   こんなバグが出ました←すごいじゃん   みんなが喜んでくれるところを探す. ○検査項目の選定 分野固有の知識,業界の常識などがないと本当に起きたらいけないことが見切れない. これまでの知識経験が生かされる. 一つのポイントとして要求仕様に書かれていることを満たしているか検査するだけでなく, 別の視点から検査をすることを心がける. ○モデル化の問題 検査したい項目が違えばモデルは異なる  はじめにモデルを作るのではなく,検査項目からモデルを作る.  検査項目がモデルを決める   検査したい項目がモデルに書かれていること.   部分モデルを作って組み合わせる.  仕様書に書いてあることだけでなく,常識などを入れた検査項目を作る.  そとの世界(外部要因)のモデル化を間違ってもいけない.  ・照明の例   停電したら 紐が切れたら 無人島だったら   リモコンでスイッチを切って出かけて停電が起きた.    壁スイッチが押されたと勘違いして照明がついてしまった. ○モデル検査作業のノウハウ  いままではモデルをちゃんと作って検査項目をいれて検査.  検査項目を作るのに時間がかかる.  最近はそこそこのモデルができたら検査器にかけて間違いをチェック  徐々にモデルの精度を上げる.  小さなモデルから複雑なモデルへ   経験的にこれぐらいの時間でやるという閾値を設定.  あたりまえことを先に検査してから下に進む.  前提条件が成立しないとtrueになるので前提条件もチェック.  あとは気楽にサイクルをまわす.    GUIによって用意にまわせるようになった.  よく知ってる人と一緒にやる. ○まとめ  モデルを作るのは大変だがシステムへの理解や知識が深まる.   11:52 講師:早水 企業におけるフォーマルメソッドの実践 ○発表内容の説明 まずはデモから モデルと検査項目はどんなモデル検査器でも必要になる. 我々はSMVをつかっています. ○モデル記述の説明 検査式(検査項目)説明   めんどくさい(通常は日本語で書いてある).  そこでモデル検査支援ソフトウェアを開発している. ○ツールの紹介 Visioの上でフローチャートを記述  フローチャートの説明   図形と意味 六角形if文など  SMVファイルの作成,モデルの完成 ○検査項目  事例でよく使うものを用意.デッドロックになってしまうとか.  範囲の指定  検査項目の穴埋めをするだけでCTL式が一発で出てくる.  ここまででSMVコードと検査項目が生成される. ツールでモデル検査を実行すると 反例(不具合の証拠)を表示してくれる.しかし読むのは大変. そこでツールが反例解析もサポート  値が変わったところを色付けしたり,状態の検索など←ここまでならexcelと同じ.  もう少しビジュアルなこともできる.  ステップ実行   反例をフローチャート上で進む様子が見られる.   通ったところは緑色で表示.  変数を選んで実行すると随時その変数の値を表示してくれる.  何がおもしろいかというとVisioなどのファイルを一式保存すれば,  2年後3年後いつでも不具合が参照できる.  一式を送信すれば遠隔地の開発者への不具合の説明が容易になる. ○モデル検査を広めるのに何をしてきたか  新しい手法は敬遠される.  経験豊かな技術者 勘と経験  導入時に勉強が必要. 一つのやり方  研究費と人手をかけて(大企業)  まずは自分で勉強してやってみる.   参考書の紹介  公的機関もセミナーを開催 結果を出してみないと効果がわかりにくい.  本当に品質が上がったのか.  まずは実践    フリーのモデル検査ツールの紹介 モデル検査の効果を数値化できない.  粘り強く継続して効果を挙げる. ○社内適用の体験談  目立つことをしてアピール  社内イントラシステムを対象に  まれにDB登録時の排他ミスがある←モデル検査は得意  解析に成功  成功したことを社内で大々的にPR  技術説明会を開催  セミナーの開講 ○なにがうれしいか  想定外の不具合がみつかる.  反例が出る.   不具合にいたる経路がわかる.   通常は不具合が発覚して原因を究明する.   検査に時間はかかるが自動化できるので,夜実行して朝チェックといった使い方もできる.  すべてパソコン上で動くので実機がいらない.  反例ファイル   いつでも再現できてプロジェクトメンバで共有できる.   社内で保存すれば反例データベースができる.  モデル検査で見つかる不具合プラス,モデル作成時に仕様の不具合が見つかる.  仕様を厳密に   例 自動販売機    ボタンを押しながらお金を入れたらどうなるか.    お金を入れて変換レバーを押す 停電したらどうなるか.  適用事例の紹介   テストをきっちり行った後のシステムで行ったら数件の不具合を発見.   全数検査の利点 ○品質向上のアプローチ  できるだけモデル検査を適用してバグを見つける. ○不具合解析のアプローチ  範囲を絞ったなかで発見された不具合だけに焦点をあてた検査を行う.  99%ぐらいの確立で不具合を発見できる. モデル検査を行っても動作試験は必要   どんな技術にも得手不得手が存在  現地で出た不具合をモデル検査で即座に発見修正←これが意外と喜ばれる. モデル検査を使うには, まずはモデル検査の理解を深める  業務の内容を理解していないのか,モデル検査を理解していないのかを明確に.   ○どの工程に適用するか   これまでは上流工程でおこなっていたが,この段階のフローは曖昧性が高い.  意外と詳細設計,コード設計への適用が効果的. まずは小さなコードから言語はC言語がおすすめ. Javaなどは工夫が必要. ブロック,関数と広げていく. 反例は保存しておくと後から見ることができて喜ばれる.   検査式の日本語からの変換が難しい.  検査式の習得が鍵  AGの位置だけで意味がまったく違う.  検査式はきっちり勉強 成果が出たら社内で大々的にアピール  局所的な社内のアピールから全社的な適用に. 12:27 質問  Q.  問題が具体的にわかっているところからモデル化しているのか.  A. モデル検査の前段階で問題の絞込みは経験者に任せる.    640憶状態で4〜5時間くらいCのステップ数で5000行から1万行.  Q. ある程度問題を絞り込んだらコードそのまま食わせるのか.  A. いけそうならそのままモデル化する.    配列などを小さくするなどの工夫をする場合もある.  Q. フローチャートは何で記述するのか.  A. 通常のVISIOではなく専用のステンシルを用いたフローチャート.  Q. モデルの正しさ,検査式の正しさをどうやって説明するか.  A. 自明な検査項目をいれて反例が出てきたら,そこを修正する.    この操作を繰り返すことでモデルがだんだん良くなっていく.    その後検査したい検査式を入れて検査する.    モデルを疑い,もうこれ以上疑う余地がなくなったら仕様書に戻る. 12:36終了