日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

Java Pathfinder における弱公平性条件の実装
太田 十字光

田辺 良則

青木 利晃

Java Pathfinder は，Java バイトコードを対象としたソフトウェアモデル検査器であり，利用者による機能拡張が容易に行えるように工夫されている．基本機能では到達可能性検査のみが可能であるが，先行研究で LTL 論理式によるモデル検査を行う機能の組み込みを行った．本研究では，弱公平性のもとでの活性検証が効率的に行えるように探索エンジンを改造した．弱公平性を LTL 論理式で記述した場合との性能比較を行い，その有効性を確認した．
Java PathFinder is a software model checker for Java byte code. It is built so that the user can easily expand
its functionality. It supports reachability check only, but there are add-in programs for model checking with
LTL formulae. In this research, we improve one of such add-in programs so that it eﬃciently conducts liveness verification under weak fairness conditions. By comparing the performance of our new implementation
against the old one with expressing the weak fairness by LTL formulae, we confirm its eﬃciency.

一部がプログラムの誤りにより停止はしないものの1 はじめに期待した動作をしない現象である．活性は並列動作すJava Pathfinder（以降，JPF） [6] は Java で記述

る複数スレッドが期待どおりに動き続ける性質のことされた並列プログラムの性質を検証できる ．並列プである．活性を確かめることで着目するスレッド間にログラムでは単一あるいは複数の目的のために，複数飢餓状態が生じないことが言える．のプロセスまたはスレッドが協調動作を行う．並列プ

JPF の基本機能である到達可能性検査はプログラ

ログラムでは複数スレッドが同時に動くことによりムの検証として有用であるが，活性検査を行えるよう固有の問題が生じ得る [7] ．例えば，デッドロックは，になれば実際のソフトウェア開発現場での有効性が一共有資源の制御順序の誤りにより並列動作するはず層高まると期待される．のスレッドが共有資源待ちとなり並列プログラムの動活性を検査する機能は JPF の基本機能で提供さ作が停止するものである．このデッドロックについてれていないが，LTL 式を扱えるように JPF を拡張

は JPF の基本機能で検査が可能である．デッドロッ

し活性の検証を可能とする研究はいくつか存在する

クと並ぶ並列プログラム固有の問題に飢餓状態があ[2] [4] [5]．本研究では，そのうちの文献 [5] による実る．これは本来並列動作するはずの複数のスレッドの装（以下これを JPFLTL と称する）をコードベースとして用いる．JPFLTL では，LTL 式の記述の一部

An implementation of weak fairness conditions in Java
PathFinder
Tojimitsu Oota, Toshiaki Aoki, 北陸先端科学技術大学院
大学情報科学系, School of Information Science, Japan
Advanced Institute of Science and Technology.
Yoshinori Tanabe, 鶴見大学文学部，国立情報学研究所
先端ソフトウェア工学・国際研究センター, School ofLiterature, Tsurumi University; Center for Global
Research in Advanced Software Science and Engineering, National Information of Informatics.

として公平性の記述が可能であり，公平性の下における活性検証が行えた．しかし，公平性を LTL 式で記述すると検査対象の状態空間が爆発的に大きくなる．
本研究では探索エンジンに，弱公平性検証のためのアルゴリズム [1] を組み込むことで，状態空間の肥大を抑えた活性検証が行えるようにした．このアルゴリズ
ムは，SPIN [3] 等の LTL モデル検査をサポートする

モデル検査器でも採用されている．

状態集合に追加し，その状態を D に積んで探索関数を再帰的に呼び出す．

2 探索アルゴリズム

探索する隣接ノードがなければ探索ループを抜けJPF の基本機能では到達可能性検査が行える．到る．今いる状態のノードが受理ノード集合に含まれ，達可能性検査は Depth First Search（深さ優先探索）かつ外側探索であれば今のノードをシードとして記憶アルゴリズムで実現される．初期状態から受理状態にし isInner を true にセットし，状態を D に積み，内至る有限長のパスが存在すれば到達可能であると判

側探索に入る．内側探索を開始したノードから遷移可断する．デッドロックの検出では，デッドロックを受能な遷移空間 A に含まれる隣接ノードを順番に調べ理状態として初期状態から受理状態へ到達するパスていく．隣接ノードが seed であるか，隣接ノードとがなければデッドロックしないことが言える．

isInner で構成する状態が D に含まれればサイクルを活性検査は，活性を検出する．活性とは初期状態か発見したことになる．内側探索中に D に存在する状ら出発した遷移列の中に受理状態を含むサイクルを態に到達すると，外側探索で受理状態を発見し，そこ無限回通るパスが存在することである．このため到から始めた内側探索で外側探索として通ったパスに到達可能性検査で使用する DFS では検出出来ない．活達したことになるため受理状態を含むサイクルを発性検査を行えるアルゴリズムは複数あるが，JPFLTL見したことになる．

では Nested Depth First Search（以降，N-DFS）アルゴリズムを採用した．

N-DFS アルゴリズムはネスト化された DFS アルゴリズムである．N-DFS の探索開始時点では外側探N-DFS アルゴリズム自体は公平性を考慮していないため，動作可能な複数のスレッドの一部だけが動作するパスを見つけて公平でない反例を報告することがある．

索として DFS を実行する．実行列中に受理状態があ

図 2 において，threadA と threadB が変数 x を共ればそこを起点（seed）として，新たに内側探索とし有している．
「いつか x の値が 1 になる」という性質て DFS を実行する．内側探索で外側探索のパスに存を考えると，実際のスケジューラ上で 2 つのスレッド在する状態を発見するとサイクルを発見，活性を検出が動作した場合，公平な動作となるためこの性質は成したと判断する．

り立つ．しかしモデル検査では全てのパスを調べるた

N-DFS アルゴリズムを図 1 に示す．概要は以下の通りである．
遷移空間を A，遷移空間の初期ノードを A.s0，スめ threadA だけが動き続けるパスを見つける．このパスでは x が 1 になることはないため反例として報告する．

タックを D，訪問済み状態集合を V，受理状態集合

検査対象は実際のスケジューラ上で動作するプログを S，外側／内側探索の区分を isInner(true=内側,ラムである．実際のスケジューラは公平性のないスケfalse=外側) とする．状態はノードと外側／内側区分ジューリングは行わない．検査対象をモデル検査するの対 (s, isInner) である．

時，活性に貢献する複数のスレッドがある場合，各ス最初に遷移空間の初期状態 (A.s0, false) を V と D

レッドが動作可能であるならそれら全てが動作した結に追加して外側探索を始める．探索関数の入り口で果として活性検出を行いたいはずである．多くの場は，スタックの一番上の状態を削除することなく取合，活性検査において公平性の適用が必要である．

り出す．取り出した状態を構成するノード，開始時点公平性には，公平性なし，弱公平性，強公平性があでは A.s0 から遷移可能な遷移空間 A に含まれる隣る．実行過程においてある時点以降あるスレッドが接ノードを順番に調べていく．訪れた状態が訪問済み「常に」動作可能であるにもかかわらず，そのスレッノード集合に含まれるか調べる．含まれていれば訪問ドがその時点以降１度も動作しない時，弱公平性は保済みであるため次の隣接ノードの検査に移る．含まれたれないと言う．実行過程においてある時点以降あるていなければその状態（ノード，isInner）を訪問済みスレッドが「無限にしばしば」動作可能であるにもかStack D = { }; // スタック
StateSpace V = { }; // 訪問済み状態テーブル
StateSapce S = nil;boolean isInner = false; // false=外側探索, true=内側探索
public void Start ( ){Add_Statespace(V, A.s0, isInner); // V に初期状態を追加．
Push_Stack(D, A.s0, isInner); // 初期状態をスタックに積む．
Search( ); // 外側探索を行う．
}
private void Search ( ){(s, isInner) = Top_Stack(D);// s から遷移可能な全ての sp を調べる．
for (each (s, 1, sp) ∈ A.T){// 受理状態がそれ自身から到達可能か調べる．
if sp == seed || On_Stack(D, sp, false){// 外側探索でこのブロックにはこない．
// 受理状態を無限回通るサイクルを発見．
PrintStack(D);PopStack(D);return;}if In_Statespace (V, sp, isInner) == false{// 初訪問の状態だった，V と D に登録する．
Add_Statespace(V, sp, isInner);
Push_Stack(D, sp, isInner);
Search( );}}if (s ∈ A.F && isInner == false){
seed = s; // 到達可能な受理状態 (外側探索)
isInner = true; // 内側探索に移る．
Push_Stack(D, s, isInner); // 現状態<s, isInner >をスタックに積む．
Search( ); // 内側探索を開始．
Pop_Stack(D);seed = nil;
toggle = false;}
Pop_Stack(D)}図1static int x = 0;
thread A {while(true) {If (x == 0) { x = 2; }else { x = 0; }}}threadB {x = 1;}
図2

検証結果が公平性に依存する例

NDFS アルゴリズム

かわらず，そのスレッドがその時点以降１度も動作しない時，強公平性は保たれないと言う．
本研究では JPFLTL に弱公平性を実装する．弱公平性を実現するアルゴリズムとして Choueka sflag construction method アルゴリズム [1] （以降，Choueka アルゴリズムとする）を採用した．Choueka
アルゴリズムの概要を説明する．
検査する遷移空間が k 個のスレッドの動作によって作られる時，遷移空間を表すオートマトン A はｋ個の要素オートマトンの積 A1 × A2 × · · · × Ak である． 今，遷移空間 A の k+2 のコピーを作り，0 番目のコピーの受理状態ラベルだけを残して残り k+1 のコピーから受理状態ラベルを取り除く．次に 0 番目のコピーの全ての受理状態から遷移して出ていく全ての遷移の行き先を 1 番目のコピーの同じ行き先状態に付け替える．i 番目 (1 ≤ i ≤ k) のコピーでは要素オートマトン Ai によって成される遷移だけを考え，その遷移の行き先を i+1 番目のコピーの同じ行き先状態に付け替える．最後の k+1 番目のコピーでは，遷移の行き先を 0 番目に付け替える．この変更によって振る舞いの追加と削除は生じない．受理状態

図3

サーチエンジンによる JVM の駆動を通る無限回のサイクルを k+2 個のコピーに展開することで，いずれかのスレッドが不公平さのために動に代表されるようなモデル記述言語で記述したモデ作できなかった場合，本来はサイクルであったはずでルと比べるとその TS の大きさは極めて大きくなる．

あるがどこかの要素オートマトンから遷移出来なくそのため普通は TS の全容を事前に知ることができななるためサイクルとはならず，受理状態を通る無限回い．JPF では，探索エンジンが Java のバイトコードのサイクルとして検出されない．従って公平性のない実行を制御しながら TS を探索していくことでメモリ反例を検出させなくなり，本来検査したかった公平な使用量を抑えている．図 3 で示すように JPFLTL のスケジューリングの下での活性検査が可能になる．

サーチエンジンが Java 仮想マシンにバイトコードをところで，本研究で実装する弱公平性は常に動作可実行させ，その結果を調べて TS 内を前進あるいは後能なスレッドについてだけ動作することを要求してい退させることでバイトコードのモデル検査を行う．

るためスレッドが常に動作可能なわけではない場合，

JPFLTL の探索アルゴリズムは前章で示した N-間欠的に動作可能であったりそうでなかったりするよ

DFS アルゴリズムと基本的に同じである．前章のうな場合，そのスレッドを公平性の対象としない．そN-DFS アルゴリズムでは同期積の全体があらかじめこである時点で動作出来ないスレッドがいた場合にそ分かっている前提であるが，JPFLTL では計算資源のスレッドを無視する動作が必要になる．i 番目の要の制限から同期積の全体を一度に知ることが出来な

素オートマトン Ai の遷移を考える時，スレッド i がい．JPFLTL では現在いる TS 内のノードと，そこそのオートマトンで遷移可能でないなら，Ai の状態から前進可能，あるいは後退可能な隣接ノードだけをから要素オートマトン Ai+1 の同じ状態へ自動的に遷考える．計算の利便のため，外側サーチのための同期移する null 遷移を加える．この null 遷移により動け積と内側サーチのための同期積を持つ．N-DFS アルないスレッドを無視することが出来る．

ゴリズムでは再帰呼び出しによって TS 内を前進ある
いは後退するが，JPFLTL では処理効率の向上を目

3 JPFLTL への弱公平性の実装的として再帰呼び出しの代わりにループを使用してJPFLTL は検査対象のプログラムをモデル M，検いる．以下に，JPFLTL の探索アルゴリズムを疑似査したい性質をクリプキ構造 K とする時，M と等価コード (図 4) で示す．

な Buchi Automaton(以降 MBA) と K と等価な BA

オリジナルの JPFLTL では公平性を LTL 式とし（以降 KBA）の同期積 (Synchronous Product) であて記述することで KBA 自体に公平性を含ませることる BA（これが遷移空間であり以降 TS）を探索する．

が出来た．しかし KBA に公平性を含ませると KBA

ところで JPF が対象とする Java バイトコードは現が大きくなる．JPFLTL が探索する TS は MBA と実的なプログラムを翻訳した命令列であり，Promela

KBA の同期積であり，KBA が大きくなると TS は/* 同期積ノードクラス SPNode */VM 状態番号;
KBA ノード;
直前のスレッド番号;
public 同期積ノード (VM 状態番号，KBA ノード，直前のスレッド番号) {VM 状態番号をセット;
KBA ノードをセット;直前のスレッド番号をセット;}/* サーチクラス SPSearch */public void サーチ () {サーチ開始を通知する ();外側同期積 = 外側サーチ用の同期積を生成する (MBA, KBA);
外側サーチ ();
サーチ終了を通知する ();}private void 外側サーチ () {外側用探索済みテーブルに現ノードを記録 (外側同期積. 現ノード ());
while(true) {if (外側同期積. 前進 ()) {深さを+1 する;
状態を前進させたことを通知する ();Node = 外側同期積. 現ノード ();if (外側用探索済みテーブルにNode が含まれる?) {// 既に訪れたノードである．
外側同期積. 後退 ();深さを-1 する;状態を後退させたことを通知する ();} else {// 初めて訪れたノードである．
外側用探索済みテーブルにNode を記録する ();}} else {if (外側同期積. 受理状態 ()) {内側サーチ ();}
状態を処理したことを通知する ();if (外側同期積. 後退 ()) {深さを-1 する;
状態を後退させたことを通知する ();} else {break;}}}}図4

private void 内側サーチ () {内側同期積 = 内側サーチ用の同期積を生成する (MBA, KBA);
内側用探索済みテーブルに現ノードを記録 (内側同期積. 現ノード ());
while(true) {if (内側同期積. 前進 ()) {// 遷移可能な隣接ノードがあった．
深さを+1 する;
状態を前進させたことを通知する ();Node = 内側同期積. 現ノード ();
位置 = 外側同期積. スタック内の位置 (Node);
if (0 < 位置) {// サイクルを発見した．
throw サイクル発見 ();}if (内側探索済みテーブルにNode が含まれる?) {内側同期積. 後退 ();深さを-1 する;
状態を後退させたことを通知する ();} else {内側用探索済みテーブルにNode を記録する ();}} else {// 遷移可能な隣接ノードがない．
状態を処理したことを通知する ();if (内側同期積. 後退 ()) {深さを-1 する;
状態を後退させたことを通知する ();} else { break; }}}}/* 同期積クラス SyncProd */スタック;
public boolean 前進 () {while (KBA に未処理のノードがあるか?) {if (MBA. 前進 ()) {KBA. 前進 ();スタックに現ノードを積む ();return true;}
MBA. 巻き戻し ();KBA. 次のリストに移る ();}return false;}
public boolean 後退 () {if (スタック内の状態が 1 個しかない?) {return false;}
MBA. 後退 ();KBA. 後退 ();スタックを POP();
return true;}

JPFLTL アルゴリズムの擬似コード

爆発的に大きくなってしまう．本研究では JPFLTL

みこんでいるため KBA のサイズは弱公平性を含まなの探索エンジンに Choueka アルゴリズムを組み込む

い LTL 式と変わらず TS サイズの増大を抑えることことで探索エンジン自体に弱公平性を適用した探索が可能となっている．

を可能とした．探索エンジン側の論理に弱公平性を組JPFLTL の主要なクラスは探索エンジンのメイン処

public boolean 前進 () {while (KBA に未処理のノードがあるか?) {if (MBA. 前進 ()) {tid = 現在の実行スレッド番号を得る;// 遷移先のコピー番号の担当スレッドが動作可能でない?
if (現在のコピー遷移空間の番号 != (-1) &&現在のコピー遷移空間の番号 != (k+1)) {if (仮想マシン. スレッドは動作可能 (tid) == false) {// null 遷移させる．
現在のコピー遷移空間の番号++;}}
KBA. 前進 ();if (現在のコピー遷移空間の番号 == (-1)) {現在のコピー遷移空間の番号 = 0;
} else if (現在のコピー遷移空間の番号 == (k+1)) {現在のコピー遷移空間の番号 = (-1);} else if (現在のコピー遷移空間の番号 == tid) {現在のコピー遷移空間の番号++;}
スタックに現ノードを積む (現在のコピー遷移空間の番号);
return true;}
MBA. 巻き戻し ();KBA. 次のリストに移る ();}return false;}
public boolean 後退 () {if (スタック内の状態が 1 個しかない?) {return false;}
MBA. 後退 ();KBA. 後退 ();スタックを POP();
現在のコピー遷移空間の番号 = スタック TOP のノードがもつコピー番号;
return true;}
図5

前進および後退メソッドの変更

理である SPSearch，探索空間 TS を扱う SyncProd，行わせる．

TS の 各 ノ ー ド を 表 す SPNode，原 子 命 題 を 扱 う

ところで，Choueka アルゴリズムでは遷移空間のAtomicProp，JPF の JVM を JPFLTL 用にラップk + 2 個のコピーを用意した．しかし，遷移空間自体する VMTotal クラスである．公平性の組み込みに関が大きいため k + 2 個のコピーを実際に用意するこ係するのは SPSerach，SPNode，SyncProd である．とは計算機資源の観点から現実的ではない．Choueka

SyncProd は JPFLTL の探索エンジンの本体である．

アルゴリズムで，k + 2 個のコピーオートマトンはオ

SyncProd が扱う遷移空間は MBA と KBA の同期積リジナルの遷移空間であるオートマトン A と全く同であるが，あらかじめ同期積全体を用意することが出じものである．唯一の違いは各々のコピーオートマト来ないため，SyncProd では KBA が遷移可能である

ンが k + 2 個のコピーオートマトンの何番目である

時 MBA が遷移可能か調べて，遷移可能であれば TSのかを意識している点である．コピーオートマトンは内の状態を一つ進めることで同期積の探索を模倣して受理状態ラベルを保持する (-1) 番目のコピー（アルいる．Java バイトコードの実行結果を調べて KBA

ゴリズムの説明では 0 番目のコピーとしたが，実装と MBA の両方に遷移可能な次状態があれば状態をでは計算の利便のため (-1) とした）と 実行スレッド

前進 (forward)，させ，遷移可能な状態がなければ状に対応した i 番目 (0 ≤ i ≤ k) のコピーと，サイクル態を戻し (backtrack)，VM に再スケジューリングをを (-1) 番目に戻すために必要な k + 1 番目のコピー

がある．TS を遷移させる時にこのコピーオートマトンの番号が分かれば実際に k + 2 個のコピーを作る必要はない．

JPFLTL に以下の変更を加えることで Choueka アルゴリズムに相当する弱公平性を実装した．図 4 の擬似コードからの変更点を説明する．
コピーオートマトンの番号を保持するために同期積ノードクラス SPNode にコピーの番号を持たせた．
また，JPFLTL が現在処理しているコピーが何番目であるのを記憶するための static 変数 (-1 から k までの値を取る) を持たせた．ノードを生成する時に，JPFLTL が現在処理しているコピーの番号を同期積ノードクラスのインスタンスに記録するようにした．
これらを，以下では，おのおの「コピーの番号」「現在のコピー遷移空間の番号」「コピーの番号をセット」

static boolean add(int a) {synchronized(lock) {if (saved >= full) {return false;}
if (saved + a >= 0) {saved += a;}if (saved >= full) {BAVerify.apValueVar("full", true);}}return true;}
public void run() {while (add(unit)) {}}public static void main(String[] args) {Saving1 t1 = new Saving1(1,0);
Saving1 t2 = new Saving1(1,1);// 並列数分スレッドを生成する．
t1.start();t2.start();// 並列数分スレッドを実行する．
}という名前で参照する．

図6

検査対象プログラム

同期積生成時に引数としてコピー番号を渡す．外側同期積の生成時は (-1) を，内側同期積の生成時は，外側サーチで受理状態を見つけた時のコピー番号を渡す．
遷移空間 TS の前進・後退を制御する同期積クラス

Saving1 t1 = new Saving1(1,0);
Saving1 t2 = new Saving1(1,1);...
Saving1 tn = new Savingn(1,n);
図7

全状態探索 (反例無し) を行うスレッドの生成に Choueka アルゴリズムを実装した．現在のコピーオートマトンが (-1) 番目の時は自動的に次のコピー条件でも測定を行った．

オートマトンに遷移する．コピーオートマトン Ai

計測対象プログラムを図 6 に示す．このプログラ(0 ≤ i ≤ k) の状態は，自身のスレッドが遷移を生じ

ムはスレッドの第 1 引数で受け取った値を saved にさせた時に次のコピーオートマトン Ai+1 の中に遷移加えていく．いつかは saved の値が full の値に達すする．コピーオートマトン Ak+1 の状態はコピーオーることが期待する性質である．LTL 論理式で表現す

トマトン A−1 の対応する状態に自動的に遷移する．

ると，♢(saved = full) となる．この論理式を検証

現在実行中のスレッドが，i 番目のコピーオートマト

対象として Java PathFinder を動作させ，生成されンで遷移を生じることが出来ない場合があるが，そのる状態数と実行時間を調べた．測定の変数として full

時には次のコピーオートマトンの同じ状態に null 遷の値を 1〜4，実効スレッド数を 2〜4 の範囲で測定を移させる．この変更の結果，同期積クラス SyncProd行った．探索は全状態探索（反例なし）と反例が見つのメソッド 前進 () および後退 () は，図 5 のようにかる２つのパターンで行った．

なる．

実験に使用した環境は Windows10 Pro，Intel Corei7 4790K，メモリ 32GB，1TB の SSD であった．JPF

4 評価実験のメモリ指定は-Xmx1024 であった．この条件で，弱公平性の適用方法として，Choueka アルゴリズ

まず，表 7 のようにスレッドを生成して，測定をムと LTL 式による弱公平性の記述を用い，この２つ行った．この場合は，各スレッドが必ず saved の増加の方法で測定を行った．また，Choueka アルゴリズに貢献するため，スレッドがどのように動いても必ずム実装のオーバーヘッドを調べるために公平性なしのsaved が full の値に達する．従って指定した LTL 式

が成立し，全状態空間が探索される．測定結果を表 1

full が 3，スレッド数 4 の時，Choueka アルゴリズムに示す．探索した状態数は，全ての条件で，公平性なの状態数は LTL 式で弱公平性を記述した場合の状態しが最も少なく，次に Choueka アルゴリズムが少な数と比べて約 20 分の 1 となった．この結果から，探かった．LTL 式により弱公平性を記述した場合の状索エンジンに弱公平性を実装することによって KBA態数が最も大きかった．のサイズを抑えることが出来，結果として TS サイズ

次に，表 7 のうち，tn のパラメタを (1,n) からの抑制につながったことを示している．

(0,n) に変更して測定を行った．最初の n − 1 個のパJPFLTL オリジナルと Choueka アルゴリズム実装

ラメタは変更していない．この場合は，並行動作するの両方でメモリの最大使用量について大きな差はな

スレッドの１つのスレッドが saved の値を増加させな

く，約 18GB だった．CPU の使用傾向については両いため，そのスレッドだけが動き続けると saved の値者で傾向に大きな差は認められなかった．各論理コアは full の値に達しない．Savings1 は値をセットするで 30〜50%程度の使用率で推移する期間と各論理コ関数で排他制御を行っているため，各スレッドが「常アがフルロードとなる期間が交互に発生した．本研究に」動作可能なわけではない．従って，Saving(0,1)

で行った実装は TS サイズ増大を抑えるための論理でのスレッドだけが動作するパスを受け入れ，それを反あり，基本的な計算方法は JPFLTL から大きな変更例として報告する．測定結果を表 2 に示す．

がないため妥当な結果である．

全ての条件で LTL 式により弱公平性を記述した場反例が見つかる場合では，予想に反して全ての合の状態数が最も少なかった．Choueka アルゴリズ

条件で Choueka アルゴリズム実装の状態数の方が明

ムの状態数はそれより多かった．公平性なしのケース

らかに大きかった．また Choueka アルゴリズム実装が最も状態数が少なかった．の探索の深さも JPFLTL オリジナルより深かった．

full またはスレッド数の一方，あるいは両方が大き

Choueka アルゴリズム適用時の TS と JPFLTL オリ

くなると TS のサイズが増大する．測定した条件でジナルの TS ではその内容が異なるため単純に比較す

表1

表2

全状態探索 (反例無し) の結果反例が存在する場合の結果

ることは出来ないが，反例検出の性能に関して何らかルの JPF と同等のサイズの問題を扱えるようにするの問題があると考えらえる．

必要がある．
謝 辞 本 研 究 の 一 部 は JSPS 科 研 費 16K00109,

5 まとめと今後の課題

26280019 の補助を受けた．

本研究では，Java PathFinder 上で LTL モデル検査を行うライブラリ JPFLTL に対し，弱公平性条件

参 考 文 献の下での活性検証を効率的に実行できるようにする[1] Choueka, Y.: Theories of automata on ω-tapes:
A simplified approach, Journal of Computer andSystem Sciences, Vol. 8, No. 2(1974), pp. 117 – 141.
[2] Cuong, N. A. and Cheng, K. S.: Towards Automation of LTL Verifcation for Java Pathfinder,
National University of Singapore, (2008).
[3] Holzmann, G. J.: The SPIN Model Checker- Primer and Reference Manual, Addison-Wesley,
2004.
[4] Lombardi, M.: JPF-LTL, https://bitbucket.
org/michelelombardi/jpf-ltl.
[5] Maeoka, J., Tanabe, Y., and Ishikawa, F.: DepthFirst Heuristic Search for Software Model Checking,Computer and Information Science 2015, Springer,
2016, pp. 75–96.
[6] Visser, W., Havelund, K., Brat, G. P., Park, S.,
and Lerda, F.: Model Checking Programs, Autom.
Softw. Eng., Vol. 10, No. 2(2003), pp. 203–232.
[7] 吉岡信和, 青木利晃, 田原泰之: SPIN による設計モ
デル検証, 近代科学社, 2008.

実装を行った．
今後の課題として，反例発見の効率が JPFLTL オ
リジナルと比較して劣っていることがあげられる．探索アルゴリズムの実装に効率的でない部分があるものと予想され改善が必要である．

Choueka アルゴリズム実装では full の値によらずスレッド数が 5 以上では完走しなかった．JPFLTL
では full=5 かつスレッド数 4 以上の条件では完走しなかった．公平性なしの検査では時間はかかるがスレッド数 5 の条件で完走した．Choueka アルゴリズ
ム実装の方が JPFLTL より扱える規模が大きいため，検査可能な問題サイズの制限は JPFLTL の性能によるものと考えられる．状態数の増大を抑えてオリジナ