数理解析研究所講究録
第 1849 巻 2013 年 71-76
2012 年度冬の LA シンポジウム [S5]71

Java 言語による確率時間 CEGAR 検証器の開発
金沢大学

小池脩平

長谷川尭志

清水隆也

山根智

Shuhei Koike, Takashi Hasegawa, Takaya Shimizu and Satoshi Yamane,Kanazawa University

1

導入．反例解析の結果，反例の候補に対応する反例が存在しないとき，同じ反例の候補を生じさせな

1.1. 背景いように抽象モデルを精錬する手法
E.M.Clarke らによって，リアクティブシステムの反例による抽象化精錬の枠組み (CEGAR) [6] のモデル検査 [4] が提案された．モデル検査ではシステム

これにより，確率時間オートマトンを対象として$CE$ -GAR を導入することが可能になった．

なお，本稿では上記の詳しい説明は省略する．本稿の状態数が大きくなる状態爆発の解決が課題になる中の記号はすべて文献 [13] と同様である．
が，述語抽象化 [7] を導入し，状態数を抑えながら検証可能な手法が CEGAR である．この CEGAR を時間確率システムに応用し，確率時間オートマトンの到 1.3

達可能性解析を可能にした確率時間 CEGAR[12] が当研究室の清水らによって提案された．
本稿では，確率時間 CEGAR を実装し，実験により得られた結果について考察する．開発言語は Javaである．

関連研究

これまで CEGAR を適用した検証手法として，リアルタイムシステムを対象とした時間 CEGAR[10] や，ハイブリッドシステムを対象とした研究 [5], 確率システムを対象とした確率 CEGAR[8], などが研究されてきた．

本研究では確率システム及びリアルタイムシステム

1.2

確率時間 CEGARの両方を併せ持つ性質を対象とするため，検証を行う上での課題として，同時実行可能性の解析手法が必要

一般に，抽象化を行うとシステムは本来の性質を損である．
なう．CEGAR[6] では，抽象モデル上での反例の候補

一方，確率リアルタイムシステムに対する検証の既[9] や PRISM[1] があの導出と，反例を用いた抽象モデルの精錬を，結論が存手法として，記号モデル検査得られるまで繰り返すことで正当性を保証するとともる．CEGAR は，状態数を抑えながら検証可能な手法に，偽反例から得た情報により，検証に必要な部分のであり，導入することで効率的な検証を期待できる．
みを詳細化することで状態数を抑えることができる．本研究では確率時間 CEGAR を計算機上に実装して，確率時間オートマトンに対して CEGAR による枠組上記手法との性能比較を行う．

みを用いて検証を行うための手法が当研究室の清水らによって確立された [13].

.
. 例の候補が実動作可能な反例であるか解析するミング言語であり，様々な実行環境で実験を行うこと検証したい性質を抽象モデルが持っていれば，具体モデルも持っている健全性を保つ抽象化手法

抽象モデルから反例の候補を導出でき，その反反例解析手法

2検証器

本研究で開発した検証器は Java により実装を行った．Java はプラッ，トフォームに依存しないプログラができ，対象となるモデルの検証結果が実行環境依存ではないという結果を得るために非常に有効であった．検証器のソースコードは 2000 行程度である．

72
3.1

FireWire Root Contention Protocol

本実験で扱う IEEE 1394 FireWire Root Contention Protocol If, IEEE 1394 FireWire 規格において，2 つの競合するノードから，一方をリーダーとして選出するプロトコルである．本実験ではこのプロトコルに対して，リーダー選出にデッドライン以上の’時間を要する場合があるかどう力$\searrow$という性質につい、$\tau.\sim.\backslash 」^{}\prime\vee.-..r_{\underline{、\geq D}}..-\backslash .--i^{\backslash }..\ldots\ldots..l’$$:\sim..-\prime.-\cdot\prime\cdots\wedge^{-}$て検証を行う．このプロトコルに対する同様の性質についての検証実験は Symbolic Model Checking[9] 及び PRISM[1] によって既に行われており，本実験では
図 1: FireWire Root Contention Protocol

確率時間 CEGAR で取り扱うゾーンは全て凸ゾー

同手法との比較を行う．

本実験では，Symbolic Model Checking[9] やPRISM [1] による検証実験で使用されたモデルを一ンであるため，ゾーンの実装には DBM[2] を用いた． 部を変更し，新たに作成したモデルに対して検証実験
DBM のように，モデルに表れる最大定数を用いて を行う．そのモデルを，図 1 に示す．新たに作成した’ゾーンを表現する場合，反例解析で用いられている前方解析が正しく行えない事が知られているが [3], 以下のいずれか 1 つ以上を満たすモデルであれば，前方.

解析を正しく行える事も知られている [3].

.

モデルでは，リーダー選出が完了したことを示すロケーション eled に不変条件 $t\geq D$ を追加している．

ここで，はリーダー選出に要した時間を表現するた$t$$D$めに，新たに追加したクロック変数である．また，はデッドラインを表す定数である．従って，eled$x_{1}-x_{2}\leq d$や $x_{1}-x_{2}<d$ を不変条件や遷移へ到達可能であることは，デッドライン以上の時間を要条件に持たない．diagonal-free なモデルである

してリーダー選出を行ってしまう場合があることを意

クロック変数の数が 3 以下のモデルである味する．

そこで本研究では，クロック変数が 3 以下のモデルのみを対象とする．

このような変更を加えるのは，Symbolic ModelChecking や PRISM では検証する性質としてデッドラインを指定できるのに対し，本手法はロケーションに対する到達可能性のみを対象としているためである．

3

時間確率システムの検証実験
本章では，確率時間 CEGAR 検証器を Java によって実装し，実験を行って既存手法とその状態数について比較する (3.1 節，3.2 節).

.
.
.
.

以下に実験環境を示す．

なお，既存手法との比較を行うため，デッドラインが 2000 から 60000 までのモデルを用意し，それぞれについて実験を行う．

このように構成したモデルに対し，Symbolic Model
Checking と PRISM で検証された性質と等価な到達可能性問題を次のように定める．

Intel Core i3- $2120T$ 2. $60GHz$$(\lambda, L_{e})=(0, \{elect\})$MemTota $13980MB$
Windows 7 Home Premium $SP$ l
Java $SE$ 1.7.0.09

すなわち，$\forall A.$

Pro $b^{A}(S_{e})\leq 0.S_{e}=\{($ elect, $v)\in S\}$を満たすかどうかについて検証を行う．この検証結果
が “No” である場合，すなわち$\exists A.$

Pro $b^{A}(S_{e})>0.S_{e}=\{($ elect, $\nu)\in S\}$

73表 1: 実験結果: FireWire Root Contention Protocol

図 2: 状態数の比較: FireWire Root Contention Pro-tocol

表 2: 状態数の比較: FireWire Root Contention Pro-tocol

図 3: CSMA $/CD$ : The Medium

基本的な通信プロトコルとして用いられており，次の手順に従って複数のクライアント間で通信を行う．

1. Carrier Sense: 通信を開始する前に，一度受信を試みることで現在通信をしているクライアントが他にあるかどうか確認する

2. Multiple Access: 複数のクライアントは同じ回線を共用し，他者が通信をしていなければ自分が真である場合，リーダー選出にデッドライン以上の時間を要する場合があることが分かる．
表 1 に実験結果を，表 2 及び図 2 に既存手法とのの通信を開始する

3. Collision Detection: 複数の通信が同時に行わ比較結果を示す．

れた場合 (コリジョン) はそれを検知し，ラン全てのデッドラインについて，既存手法よりも少ない状態数で検証を終えている．また，状態数の推移から，デッドラインの小さいうちは効果が少ないものの，デッドラインの増加に伴い，状態数がより削減さダムな時間待ってから再び送信手順を行う
本実験ではこのプロトコルに対して，各クライアン
トが通信を完了するのにデッドライン以上の時間を要する場合があるかどうか，という性質について検証れていることがわかる．

3.2$CSMA/CD$を行う．このプロトコルに対する検証実験は 3.1 節と様に Symbolic Model Checking[9] 及び，PRISM[ ]. よって既に行われており，本実験では同手法との比$\Pi\overline{p}$
$I$

$I$

$|’$
$1$

本実験で扱う CSMA/ $CD$ (Carrier Sense Multiple

Access/Collision Detection) は，Ethernet における]$\mathfrak{B}$を行う．

74
表 3: 実験結果: $CSMA/CD$ (bcmax $=1$ )$\triangleright,^{--m}.;_{\mathfrak{n}\{\dot{b}c+1.\iota,ma\}}^{l-\cdot 0}x.s_{b_{t}u\gamma,}b..k)x$

表 4: 実験結果: $CSMA/CD$ (bcmax $=2$ )図 4: CSMA/$CD$: The Stations

本実験で使用するオートマトンを図 3 及び図 4 に示す．図 3 はクライアント間の通信の伝送路の挙動を表現したものであり，図 4 は通信を行うクライアントの挙動を表現したものである．今回の実験に用いる実際のモデルとしては 2 つのクライアント間を伝送路で繋いで通信を行うことを想定しており，これらの 3つのオートマトンを並列合成したモデルとなる．ここで用いられる bcmax とはコリジョンが発生した場合に行われる再送処理を行う回数の上限である．

このように構成したモデルに対し，検証性質となる

到達可能性問題を次のように定める．
$(\lambda, L_{e})=(0, \{DONE\})$いる．この実験の際にログを追ってみると，ループを含んだロケーションにより多くの述語が追加されることによって，状態が細分化されていることが判明した．FireWire Root Contention Protocol のモデノレではループが 2 カ所であったが，CSMA/ $CD$ のモデル
ではループが 16

すなわち，$\forall A.$

Pro $b^{A}(S_{e})\leq 0.S_{e}=\{(DONE, v)\in S\}$を満たすかどうかについて検証を行う．この検証結果が$N\circ^{))}$である場合，すなわち$\exists A.Prob^{A}(S_{e})>0.S_{e}=\{(DONE, \nu)\in S\}$が真である場合，各クライアントが通信を完了するのにデッドライン以上の時間を要する場合があることがわかる．

表 3 及び表 4 に実験結果を，表 5, 表 6, 図 5 及びではないかと考えられる．

4

まとめ

本研究では，確率時間オートマトンの到達可能性解
析において，CEGAR による枠組みを適用した検証手法を実装し，実験によって一定の効果が得られるこ.とを示した．本論文の主な貢献は以下である．

bcmax $=1$ かつデッドラインが 1800 及び 2000 のときには既存手法よりも状態数が大きくなってしまって本手法を実装して実験を行い，既存手法と比較し，特定のモデルにおいて，より少ない状態数での検証が可能であることを示した

bcmax $=2$ のときについては，デッドラインが既存手法よりも少ない状態数で検証を終えているが，所にもなり，これにより CEGARループの回数が増え，状態数が増えてしまっているの

図 6 に既存手法との比較結果を示す．

1000 のときを除き、 すべてのデッドラインについて$\chi$.

今後の課題として，以下のことが挙げられる．
本手法をモデル検査に拡張し，PTCTL による到達可能性以外の性質の検証

75
表 5: 状態数の比較:CSMA/ $CD$ (bcmax $=1$ )$1R1m,\overline{\overline{\sim*sp_{i}vQ*b\triangleright\cdot*\ovalbox{\tt\small REJECT}_{\mathcal{M}dt\iota}^{w(\kappa\Gamma l\propto n}u_{-}\phi},..\cdot\ldots\ldots..\cdot../^{\prime^{\prime^{\backslash }}}:\cdot:..------\overline{/}\prime’-/^{\prime^{\backslash }}/^{\backslash }\ldots.\cdot\ldots.\bigwedge_{\backslash }}$$1$$\overline{:\ldots\cdot\cdot\cdot\cdot\cdot\cdot\cdot\cdots\cdot\cdots\cdot=}\cdot\underline{\wedge\cdot\cdot\cdot\cdots\cdot\cdots\cdot}-r^{i:}/^{\backslash}-\sim\sim-\cdot-*$$arrow$$1\infty.$$-\vee\backslash$$10 1M \infty-\overline{m}$$M\mathfrak{U}\cdot(bc\mathfrak{m}rl\}$

図 5: 状態数の比較:CSMA/ $CD$ (bcmax $=1$ )表 6: 状態数の比較:CSMA $/CD$ (bcmax $=2$ )$1K_{\overline{\prime}}:_{\ovalbox{\tt\small REJECT}^{*bQ\#tAlut*cn*\iota m}..\backslash }\prime_{\frac{}{\ovalbox{\tt\small REJECT}^{P\aleph \mathfrak{d}}}}\vee,m\eta_{Kk\aleph}..\cdots\cdots t\vee^{\wedge}$:$|^{1m_{h}}:\};:$$\wedge-$$-\cdot\cdot--::\wedge^{arrow}\prime\prime..:::.\cdots\ldots\cdots\cdots\cdots\cdot\cdot\cdots\cdot\cdots\cdot.\cdots\cdots$$*\cdot\cdot:\ldots-\cdots\cdots\cdots\cdot\cdot-*-*-\cdot\cdotarrow\sim\cdot\cdotarrow--$$1\infty$

:

$10$

$1r$

, $m_{-}m$$\overline{zmr}-.$$1m\ldots..$。回 $\infty(bmR\rangle$.

図 6: 状態数の比較:CSMA/ $CD$ (bcmax $=2$ )既存手法よりも状態数が多くなったモデル等で有効な状態数削減手法の考案

確率時間オートマトンに対する検証手法である
Symbolic Model Checking [9] では，PTCTL (Probabilistic Timed Computation $hee$ Logic) によって性質を記述したモデル検査が可能であるが，確率時
間 CEGAR では PTCTL で表現可能な性質のうち到達可能性のみ検証可能である．一方，CEGAR を用いた PTCTL のサブクラスによる性質について検証可能な手法として，確率時間 WiGAR[11] が提案されている．この手法では PTCTL のサブクラスではあるが，到達可能性のみならず，いくつかの性質について CEGAR を用いた検証が可能であることが報告されている．

FireWire Root Contention Protocol においては成果が得られたが，CSMA $/CD$ においては本手法が有効であるとは言い難いため，様々なモデルで状態数の削減が望める手法を考案する必要がある．そのためには，より多くのモデルにおいて確率時間 CEGAR 検証器を適用させ，原因を特定した上で，解決策を模索(していくことが今後の課題といえる．

参考文献[1] Prism -probabilistic symbolic model checker.
http: $//www$ . prismmodelchecker. $org$ , アクセス:2013 年 1 月 17 日．

[2] Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. InLNCS, Vol. 3098, pp. 87-124, 2004.
[3] P Bouyer. Untamable timed automata! LNCS,Vol. 2607, pp. 620-631, 2003.
[4] E. M. Clarke, Orna Grumberg, and DoronPeled. Model checking. MIT, 2000.

[5] Edmund M. Clarke, Ansgar Fehnker, Zhi Han,
Bruce H. Krogh, Joel Ouaknine, Olaf Stursberg, and Michael Theobald. Abstraction andcounterexample-guided refinement in model
checking of hybrid systems. In IJFCS, Vol. 14,
pp. 583-604, 2003.
[6] Edmund M. Clarke,
Orna Grumberg,
Somesh Jha, Yuan Lu, and Helmut Veith.

76
Counterexample-guided abstraction refinement. In LNCS, Vol. 1855, pp. 154-169,

2000.
[7] Susanne Graf and Hassen Saidi. Constructionof abstract state graphs with PVS. In LNCS,
Vol. 1254, pp. 72-83, 1997.

[8] Holger Hermanns, Bj\"om Wachter, and LijunZhang. Probabilistic cegar. In LNCS, Vol. 5123,pp. 162-175, 2008.
[9] Marta Kwiatkowska, Gethin Norman, JeremySproston, and Fuzhi Wang. Symbolic model
checking for probabilistic timed automata. InInformation And Computation, Vol. 205, pp.

1027-1077, 2007.
[10] M. Oliver Moller, Harald Rues, and Maria
Sorea. Predicate abstraction for dense realtime systems. In Electronic Notes in TheoreticalComputer Science, Vol. 65, pp. 218-237, 2002.

[11] 高橋正樹，清水隆也，山根智．確率時間 WiGAR
による PTCTL サブクラスのモデル検査．数理解析研究所講究録，第 1744 巻，pp. 25-34. 京都大学，2011.

[12] 清水隆也，森下篤，山根智．確率時間 CEGAR の開発とその実証実験．情報処理学会論文誌プログラミング ( $PRO$ ) , Vol. 5, No. 2, pp. 43-66,

mar 2012.
[13] 清水隆也，森下篤，山根智．抽象化洗練を用いた時間確率システムに対する形式的検証手法 (アルゴリズムと計算理論の新展開). 数理解析研究所

講究録，Vol. 1799, pp. 29-36, jun 2012.