産業ソフトウェア

表6.1: キュー問題のケーススタディ結果

１つのエラー 最短パスのエラー すべてのエラー

1度目 2度目 1度目 2度目 1度目 2度目

遷移(Transitions) 58,372 176 199,063 1,791 (failed) 1,791 メモリ量 (MB) 70 65 110 65 65

時間 (msec) 97 3 690 4 2

エラーの数 1 1 364 4 6

反例の長さ(lines) 287 82 88 82

-$ % &

&RQYH\HU6\VWHP

(QWU\ 0RGXOH$ 0RGXOH% 0RGXOH&

ฎ⌮ෆᐜ

䝛䝑䝖䝽䞊䜽㏻ಙ

䝀䞊䝖 䝉䞁䝃

≀య 䝧䝹䝖

䝁䞁䝧䜰

⤌㎸䜏䝋䝣䝖 ⤌㎸䜏䝋䝣䝖 ⤌㎸䜏䝋䝣䝖 ⤌㎸䜏䝋䝣䝖

図6.2: 搬送システムの概要(再掲)

䝰䝕䝹ᢳฟ

;WKDͬDͿ

ᛶ㉁ᐃ⩏

䝰䝕䝹᳨ᰝ

;^W/EͿ ኚ᥮䝹䞊䝹㞟ྜ

䛾ᵓᡂ

䝋䞊䝇䝁䞊䝗

;Ϳ

ᨾ㞀 ᛶ㉁

᳨ド䝰䝕䝹

;WƌŽŵĞůĂͿ 䝹䞊䝹ኚ᥮

㞟ྜ

⤖ᯝゎᯒ;཯౛Ϳ

≧ែ⇿Ⓨ

ᨾ㞀䜢෌⌧

;ϲͿ

;ϰͿ

;ϱͿ

;ϭͿ;ϮͿ

;ϯͿ

䝣䜷䞊䝹䝖 䠄⤊஢䠅≉ᐃ

;ϲͿ ഇ཯౛

図6.3: 実施した手順

6.2.2 実施条件

本ケーススタディに関わった参加者のタスクについて，表6.2に示す．第一の参加者は，

QVToの実装に関して３カ月の経験を持っていた．一日間のターゲットシステムの構造お よび運搬仕様の教育を受けた．第二の参加者は，ターゲットシステムの開発に参加し，シ ステムの全体の仕様と設計を理解していた．両参加者は，モデル検査の経験を持っていた．

分担としては，主に第一の参加者がルールの設計記述を行い，第二の参加者がモデル検査 の実施と，抽象化の設計を行った．

ユースケースの際には，次の最低限の情報が与えられていた：

• デッドロックを発生したことで内部の状態遷移がストップした

• モジュール間のメッセージ送受信において特定のシグナルを送ったときに発生する

6.2.3 フォールトアナリシス手順

図6.3に，実施したフォールトアナリシスの手順を示す．

1. 抽出するモデルの設計: モデルとして抽出するソースコードの範囲と，外部環境と して抽象化する範囲の境界を定める．例えば，ハードウェアを操作する関数はすべ て空のスタブ関数に置き換える，あるいは，モジュール間の通信をグローバル変数 の読み書きに置き換えるなどが考えられる．

表6.2: ケーススタディの参加者

# 変換ルール モデル検査 製品ドメイン

1 √ √

(√ )

2 - √ √

2. モデル変換ルール集合の構成: 上記のモデルの設計に従って，一般的な（POM/MC が標準で持っている）モデル変換ルールを選択するか，対象とするソフトウェアや 問題にあわせてモデル変換ルールを新たに作成する．

3. プロパティの定義: 検査したいプロパティをLTL式またはassertionとして定義する．

4. モデル抽出: POM/MCにソースコードと上記で構成したモデル変換ルール集合を 与え，Promelaコードを自動抽出する．

5. モデル検査: POM/MCからSPINを起動し，抽出したモデルがプロパティを満たす か否かを検査する．

6. モデル検査結果の評価: モデル検査の結果を評価し，対象となる故障を発見できた か否かを決定する．SPINがプロパティ違反を発見した場合，反例トレースが対象と する故障に至る振る舞いを表現していることになる．もし，反例トレースが示す振 る舞いが対象のソースコードでは発生しないものである場合や，状態爆発が起きた 場合には，ステップ(1)またはステップ(2)に戻る．ケーススタディにおいては，モ デル検査が2時間で終了しない場合には，状態爆発が発生したと判断した．

6.2.4 結果

表6.3に示したように，7回の試行錯誤によって，対象となる故障を再現した．特徴的 なステップについて説明する．モデル検査が状態爆発で実施できない場合には，モデル変 換ルールを再構成してターゲットモデルを抽象化することで，さらに状態空間を縮小する 必要があった．例えば，表6.3のステップ3では，モジュール間通信に伴う状態数を削減 するため，パラメタを受け渡すプロセスをバイパスしプロセス間で直接通信するモデル変 換ルールを適用した．しかし，モデル検査によって得られた反例は，元のソフトウェアで は発生しえない偽反例であった．偽反例を得た場合には，抽象化を緩めるか，異なる抽象 化の方法を採用する必要がある．ステップ4では，ステップ3での抽象化をやめ，ネット ワークを単純化する抽象化を行った．結果，再び状態爆発が発生したため，ステップ5で はネットワークをさらに単純化した．このように，抽象化を試行錯誤的に繰り返すことで，

ステップ8において故障の再現に至った．

図6.4に，各ステップでのPromelaモデルの行数と，Promelaモデルに含まれるシンボ ルの数の変化を示した．抽象化によりモデルを縮退していた様子が見てとれる．

以上のステップで故障を再現するのに，約4日間，工数にして7人日を要した．反例を 分析するためのソースコードやドキュメントの調査時間は含んでいる．ただし，対象シス テムの調査や，POM/MCおよびSPINの実行時間は含んでいない．元のソースコードは 約17,000行であり，最終的に抽出されたモデルは，Promelaで約2,000行（コメント行等 を除く）であった．

図6.4: 段階的なモデルの抽象化

表 6.3: フォールトアナリシスの経緯

# 変換ルールの内容 (差分) 結果 1 ドライバ作成，ハードウェア動作模擬 (搬

送制御,通信,シグナルの発生)

状態爆発 2 ハードウェア動作模擬の追加 (シグナルの

処理)

状態爆発 3 縮退の追加 (関数引数処理の簡略化) 偽反例 4 縮退の追加 (通信前処理の簡略化) 状態爆発 5 縮退の追加(通信前処理のさらなる簡略化) 偽反例 6 ハードウェア動作模擬の追加 (モジュール

間の同期処理)

状態爆発 7 縮退の追加 (タイムアウト処理の削除) 偽反例

8 縮退の追加 (タイムアウト処理の簡略化) フォールト特定成功