二度目の試行

故障状態f rと故障条件Ctは維持する．一度目の結果により，並行性に関する予測は棄 却されなかったため，h1は仮説として維持し，一度目の試行で得られた新たな仮説を加え

ることとした．f t^′₁が故障に関係する状態であることから，関数nondet intによる値の非 決定性は故障に関係がないという仮説と，キューのサイズは故障に関係がないという仮説 を加えてh₂とした．

h₂ = {“Concurrency caused the ERROR”,

“N ondeterminism doesn^′t relates to the ERROR”

“Size of queue doesn^′t relates to the ERROR”}

そこから，並行実行において，値を固定値にして，キューのサイズを最小にしても，故 障が発生するという予測Pd2を導出した．

Pd2 = {(“Concurrency” and“f ixed value” and“minimal queue size”,

“ERROR”)}

故障再現フェーズ(2)

予測Pd2の事前条件に加えた“fixed value”は，non_detint関数の動作を変更すること で実現できる部位仮説であるため，対応するスタブ変換ルールを選択した．しかし，キュー のサイズはマクロで定義されており，C言語モデルで表現されるASG上ではキューのサ イズは具体値に展開されているため，モデルの変換ではキューのサイズの変更は困難であ ると判断した．そのため，キューのサイズについては，手作業でマクロ定義を変更した．

R₂ = (P threads, StubF unction) φ₂ = ¬“ERROR”

一度目と同様，φ₂は表明を用いて検出できるため，対応する変換ルールをR₂に加えた．

R₂= (P threads, StubF unction, Assertion)

選択したモデル変換ルール集合を用いてPromelaモデルを生成した．反例ce₂を得た．

ce₂ =pommc(R₂, sc(p), φ₂)

確認フェーズ(2)

モデル検査により，故障条件Crを満たす再現故障f r^′₂を得た．

f r^′₂ = (“Error in t2”, i= 2, stored elements[i] = 0in t2)

また，反例ce2を解析することで，f t^′₂▷_{pom(R2,sc(p))}f r₂^′)を満たす状態として，スレッド t₁が動作する前に，スレッドt₂が動作しカウンタiを加算した状態f t^′₂が見つかった．

f t^′₂ = (“t₁ not run”, i= 1 in t₂)

図6.1に，正常動作時と故障発生時のシーケンス図を示す．本シーケンス図は，POM/MC が反例として生成したシーケンス図を簡約して作成したものである．反例の解析によって，

stored_elements

main t1 enqueue_flag queue dequeue_flag t2

set (TRUE)

set (FALSE)

create() check(TRUE)

set(FALSE)

set(TRUE)

check(TRUE)

set(FALSE) dequeue() set(TRUE)

enqueue (value ) create()

set(0, value)

get(i) i=0

(set,getはコード上は変数アクセス)

stored_elements

main t1 enqueue_flag queue dequeue_flag t2

set (TRUE)

set (FALSE)

set(TRUE)

check(TRUE)

set(FALSE) dequeue() aet(TRUE)

create()

get(i) create()

set(FALSE) check(TRUE)

enqueue (value )

set(0, value) i=0

i++

check(TRUE)

不整合

図6.1: キュープログラムのシーケンス図

２つのスレッドが特定の順で実行される時に故障が発生することがわかった．つまり，ス レッドt₂がスレッドt₁より先に実行した場合，deque_flagがFALSEのためデキューを しないまま，カウンタiのインクリメントのみをすることがある．

そこで，スレッドt₂が，スレッドt₁より先に動作を開始することをフォールト条件Ct とした．

Ct= “t1 not run ,“t2 run”

実際，元のソースコードを精査すると，Ctを満たす状態が発生しうることがわかった．こ れが故障の原因となるフォールトであると結論づけた．

まとめ

本ケーススタディは，Intel⃝Core^{R TM}i7-3770 CPU (3.4 GHz)と16GBのメモリを搭載 し，Windows⃝7 Ultimate^R を搭載したPCで実施した．モデル検査に用いた計算機リソー スは図6.1にまとめる．各試行において，SPINのオプション3種を試した;エラーを１つ のみ見つける(-c1)，最短パスのエラーを見つける(-i)，すべてのエラーを見つける(-e)で ある．SPINが探索した状態空間(SPINの出力としては Transitions=stored statesの数 と matched statesの数の合計)や，モデル検査にかかる時間は，1度目の試行に対して2 度目の試行は著しく減少している．1度目の試行での，すべてのエラーを見つける場合に は，メモリー不足によりモデル検査が失敗した．また，反例トレースの長さもモデル抽象 化によって短縮した．短い反例トレースは長い反例トレースよりもフォールトの特定は容 易であろうと考えられる．

表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: 搬送システムの概要(再掲)