Efficient Scenario Verification for Proximity-based Federations of Smart Objects Using Symbolic Model Checking

記号モデル検査によるスマートオブジェクトの近接連携シナリオの 効率的な検証 *

蓑田玲緒奈

^†a)

湊 真一

^†b)

Efficient Scenario Verification for Proximity-based Federations of Smart Objects Using Symbolic Model Checking

^∗

Reona MINODA

^†a)

and Shin-ichi MINATO

^†b)

あらまし ユビキタスコンピューティング(UC)シナリオの検証は，UCの様々なアプリケーションを設計す る際に，設計上の問題を実装の前段階で発見できるため有用である．本論文では，Context Catalytic Reaction Network (CCRN)で記述されたUCシナリオの記号モデル検査による検証を提案する．具体的には，CCRNを 記号モデル検査問題に変換することで，筆者が過去に提案した素朴な手法では検証が困難であった大規模なUC シナリオの検証を現実的なコストで可能になることを実験的に示す．また，同じ枠組みでUCシナリオの有界モ デル検査による欠陥検出の有用性についても実験的に示す．

キーワード ユビキタスコンピューティング，触媒反応ネットワーク，形式検証，記号モデル検査，スマート オブジェクト

1.

^{ま え が き}

ユビキタス・コンピューティング

(UC)

では，様々 なモノが連携し合う．これらのモノを本論文でスマー トオブジェクト

(Smart Object, SO)

と呼ぶ．

PC

，携 帯電話，組み込みコンピュータなどの計算や通信機能 を有するデバイスはもちろん

SO

とみなすことができ るが，食べ物や食器，コップなど一見すると計算や通 信機能を有していないモノも，

RFID

タグなどを貼り 付けてしまえば，

SO

とみなすことができる．本論文 でフェデレーションとは複数の

SO

が近づいたときに 起こる現象を指すことにする．フェデレーションの例 としては「薬の瓶と飲み合わせの悪い食べ物が近づ いたときに，ユーザのもっているスマートフォンで注 意を促す」といったことが考えられる．本論文で扱う

UC

シナリオとは複数のフェデレーションが介在する

†北海道大学大学院情報科学研究科，札幌市

Graduate School of Information Science and Technology, Hokkaido University, Sapporo-shi, 060–0814 Japan a) E-mail: [email protected]

b) E-mail: [email protected]

*本論文は学生論文特集秀逸論文である．

DOI:10.14923/transinfj.2017PDP0037

現象のことである（図

1

）．

UC

の分野では様々なフ レームワークが提案されてきているが，これらのフ レームワークは多くの場合「位置に限定されない遍在 的なサービス」と「場所に応じて提供される状況依存 性のあるサービス」の

2

種類のアプリケーションシ ナリオを対象としており，それらにとらわれない様々 な種類のアプリケーションシナリオを議論するために は

UC

シナリオの形式的議論が重要であると田中は 指摘し，形式的議論のための基本的なアイディアを提 案した

[1]

．その後，

Julia

と田中によって

UC

シナリ オを記述する触媒反応ネットワークモデル

[2]

が提案 されたが，形式検証する手法が確立されておらず課題

図1 UCシナリオの例 Fig. 1 Example of a UC scenario.

となっていた．これに対して筆者は，触媒反応ネット ワークモデルに対してセグメントグラフと呼ばれる要 素を導入した

Context Catalytic Reaction Network (CCRN)

を提案し，

CCRN

のモデル検査問題への変 換手法を提案することによって，

UC

シナリオをモデ ル検査で検証することを可能にした

[3]

．この手法によ り，

UC

シナリオの様々な性質を議論することが可能に なった．具体的には，以下のようなことが可能になった．

•

時相論理で記述された性質（例えば，ある特定 のフェデレーションがある条件の後でいずれ起こる）

を満たすかどうかを，

CCRN

で記述された

UC

シナ リオから判定

•

上記の性質を満たさない場合があるならば，反 例を提示

この種の検証で最も重要な側面は，このような

UC

シ ナリオの性質に関する議論を設計段階で行うことがで き，追加のコストがかかる実装段階になる前にそれが 行えることである．

しかし，この変換手法はある種の素朴なアプローチ であったため，大規模な

UC

シナリオの検証のための スケーラビリティの向上が課題であった．本論文では，

CCRN

の検証のスケーラビリティを向上させるため に記号モデル検査を用いた手法を提案する．記号モデ ル検査は大規模な状態遷移系の検証をするための手法 の一つであり，

McMillan

らによって確立された手法 である

[4]

．本論文では，

UC

シナリオの検証問題をモ デル検査問題に帰着させる際の記号モデル検査の活用 方法を示す．更に，素朴な手法では検証できなかった より大規模な

UC

シナリオが本論文で提案する手法を 用いることで検証可能になることを実験的に示す．

更に，記号モデル検査による検証手法と同様の枠組 みで有界モデル検査と呼ばれる検証手法を活用するこ とができることが知られている

[5]

．有界モデル検査 は多くの場合モデル検査問題の反例を記号モデル検査 よりも高速に見つけることができるため，有界モデル 検査はモデルの欠陥を検出する目的で広く使われてい る．本論文では，有界モデル検査が

UC

シナリオの検 証問題でどの程度実用的なのかについても実験的に評 価をする．

本論文は国際会議

PECCS2017

の予稿集の一つとし て採録済みの内容

[6]

に対して，特に有界モデル検査 による

UC

シナリオ欠陥検出に関して，より詳細な評 価実験を行った内容を追加した拡充版である．

本論文の構成は以下のとおりである．

2.

^{では，本研}

究の関連分野の研究について紹介をする．

3.

では，表 記や提案手法に必要な要素である

CCRN

や記号モデ ル検査についての準備をする．

4.

^{では，これらの準備} を踏まえて，記号モデル検査による

CCRN

の検証手 法についての提案をする．

5.

では，本手法について記 号モデル検査と有界モデル検査の二つの側面からの評 価を実験的に行う．

6.

では，本論文の貢献について結 論をまとめる．

2.

関 連 研 究

本章では，

UC

分野で設計上の不具合の検出や不適 切な振る舞いの検出を行う関連研究紹介する．

サイバーフィジカルシステム

(Cyber Physical Sys-

tem, CPS)

と呼ばれる，多くのセンサーデバイスが

気温や加速度などのような物理的現象を測定し，この 測定結果を踏まえて自動化ロボットのようなアクチュ エータが物理世界を操作することでフィードバックす るような系を対象とした分野では，個々のセンサーや アクチュエータなどの組み込みシステムの動作を形式 検証する研究があり，

Herbar

らなどが検証フレーム ワークを提案している

[7]

．これらは，個々のデバイス のハードウェアや組み込みソフトウェアの動作の検証 が主な目的でありこれらのデバイスを動的に連携させ るシナリオの検証は行っていない．また，物理世界に 適切なフィードバックを行うために，センサーから得 られた情報から物理世界の状況を判断するルールセッ トの整合性が取れているかどうかを検証する研究も見 られ，

Sun

らなどが検証フレームワーク提案してい る

[8]

．しかし，これらはリアルタイム性を重視した検 証を行うことが多く，事前に網羅的検証を行うモデル 検査とは異なり，検証にもれが生じる可能性がある．

アンビエント・コンピューティングの分野では，コ ンテクスト不整合検出

(context inconsistency detec- tion)

を目的としたフレームワークを

Xu

らなどが提 案している

[9]

．この手法は「ユーザが部屋に入った」

や「部屋の気温は

30

^◦

C

である」のような収集された イベントのシーケンスから，イベント同士の不整合を 論理的推論によって検出する．この手法は形式検証と は違い，系が実際に動き始めた後に適用できる手法で あるため，設計段階で問題のあるふるまいなどをあら かじめ見つけることができない．

3.

^{準 備}

本章では，以後の説明に必要な定義，表記，要素に

図2 触媒反応の例

Fig. 2 Example of a catalytic reaction.

ついて説明する．

3. 1

基本的な定義と表記

X

^と

Y

を任意の集合とするとき，

X ∪ Y

^，

X ∩ Y

^，

X \ Y

をそれぞれ

X

と

Y

の和集合，積集合，差集合 とする．集合

X

^{について，}

2

^Xを

X

^{の冪集合（すな} わち，全ての部分集合）とし，

|X|

を

X

^{の要素数とす} る．また，集合族（すなわち，集合の集合）

M

^につい て，

M

に含まれる全ての集合の和集合と積集合をそ れぞれ

M

，

M

と表記する．

3. 2

触媒反応ネットワーク

触媒反応ネットワークは元々生物の分野でタンパク 質の代謝を分析する目的で

Stuart Kauffman

によっ て提案されたものである

[10]

．このモデルを基づいて，

田中はこれを

SO

の複数のフェデレーションが相互に 関わる

UC

シナリオを記述する方法として

UC

の分野 に適用した

[1]

．本論文では，触媒反応ネットワークは 後者を指すものとする．

触媒反応ネットワークは触媒反応の集合である．各々 の触媒反応は複数の物質を入力としてそれを別の複数 の物質に変換し，それを出力とする．また，各々の触

媒反応は

context

と呼ばれる触媒をもつ．また，入力

の物質に触媒を含ませることもでき，このような種類

の触媒を

stimulus

と呼ぶ．触媒反応は全ての必要と

される

SO

が互いに近傍に位置するときに起こる．こ こで

SO

の近傍領域の内側を

scope

という言葉で表現 することにし，

SO o

^の

scope

は

SO o

^{から通信でき} る

SO

の集合として表現する．文献

[1]

では，全ての

context

と

SO

の

scope

が考慮されているが，本論文 では

context

の

scope

のみを考慮するものとする．言 い換えると，全ての必要な

SO

が

context

の

scope

に 入ったときに，その

context

に対応する触媒反応が起 こるものと本論文では扱う．

図

2

は単一の触媒反応の例である．この触媒反応で は，

context

としてゲート

c

1があり，ユーザは電話

a

，

図3 4種類の触媒反応

Fig. 3 Four Types of catalytic reactions.

ヘッドセット

b

^，

IC

カード

s

^の三つの

SO

をもってい る．ユーザが

c

1の

scope

に入ると，

c

1は

a

と

b

に連 携するように働きかける．この動作は

s

^{がきっかけと} して起こる．この動作の後，電話

a

^{とヘッドセット}

b

はフェデレーションを形成する．本論文では，

a

^と

b

によるフェデレーションを

a

と

b

の連結（すなわち，

ab

）で表現する．この動作では

c

1 と

s

は触媒として 働いている．特に

s

^{はこの触媒反応の}

stimulus

であ る．この反応を図

2

の右側のように表記する．

触媒反応ネットワークには，図

3

に示すような

4

種 類の触媒反応がある．

4

種類の触媒反応は大きく二つの グループに分けられ，一つは合成反応のグループ（図

3 (i)

と

(ii)

），もう一つは分解反応のグループ（図

3 (iii)

と

(iv)

）である．図

2

の触媒反応は図

3(i)

の種類 に属している．また，図

3 (ii)

のような

stimulus

がな い触媒反応も考えることができる．図

3 (ii)

では，

SO a

と

SO b

をもったユーザが

stimulus

なしで

context c

^2の

scope

に入ることだけをきっかけに，

c

^2は

a

^と

b

に連携するように働きかける．同じようにして図

3 (iii)

や

(iv)

のような分解反応も考えることができる．

図

3 (iii)

のような種類の反応では，ユーザが

ab

^とい うフェデレーションを形成している

SO a

と

b

と更に

SO s

^をもって

context c

^3の

scope

に入ると，

c

^3は

stimulus s

をきっかけとしてフェデレーション

ab

^を 分解する．図

3 (iv)

の触媒反応は図

3 (iii)

の

stimulus

がない触媒反応である．

触媒反応の出力となる

SO

は，

stimulus

として他の 触媒反応を促進したり，他の触媒反応の入力の

SO

と なったりする．このようにして，複数の触媒反応によ り触媒反応ネットワークを形成する．

ここで，触媒反応ネットワークを形式的に定義する．

まず

O

を

SO

の集合とする．フェデレーションを形 成している

SO o

f を

o

f

∈ 2

^O

\ ∅

と定義する．なお，

|o

f

| = 1

のときは

o

f はフェデレートしていない単一 の

SO

とみなせる．次に触媒反応を以下のように定義 する．

［定義

1

］（触媒反応）

O

と

C

をそれぞれ

SO

と

con- text

の集合とする．触媒反応はタプル

( c, M, N )

と定 義される．ただし，

• c ∈ C , M ⊆ 2

^O

\ ∅ , N ⊆ 2

^O

\ ∅

• ∀o

f

∀o

_f

∈ M. ( o

f

= o

_f

→ o

f

∩ o

_f

= ∅ )

• ∀o

f

∀o

_f

∈ N. ( o

f

= o

_f

→ o

f

∩ o

_f

= ∅ )

•

M = N

• (|M ∩ N| + 1 = |N |, |M | > |N |) ∨

( |M ∩ N | + 1 = |M |, |M | < |N | ) ( ∗ )

である．

なお，

(*)

で示した最後の条件の前半と後半部分はそ れぞれ合成反応と分解反応で満たすべき条件を表して いる．

ここで，この定義を用いた触媒反応の例を与える．

C = {c

1

, c

3

}

^，

O = {a, b, s}

^{とすると，図}

3 (i)

と

(iii)

の触媒反応はそれぞれ

( c

1

, {{a}, {b}, {s}}, {{a, b}, {s}} )

，

( c

³

, {{a, b}, {s}}, {{a}, {b}, {s}})

と表現することができる．

最後に触媒反応ネットワークを以下のように定義 する．

［定義

2

］（触媒反応ネットワーク） 触 媒 反 応 ネット ワ ー ク

R

は 触 媒 反 応 の 集 合 で 定 義 さ れ る ．た だ し，

∀r, r

∈ R. ( c = c

) where r = ( c, M, N ) , r

= ( c

, M

, N

)

．

3. 3 Context Catalytic Reaction Network Context Catalytic Reaction Network (CCRN)

は，

触媒反応ネットワークに関係する

SO

の状況を表現す る離散構造である

[3]

．前節で述べたように，触媒反応

は必要とされる

SO

が全て対応する

context

の

scope

に入ると起こる．触媒反応ネットワークの性質を状態 遷移系として分析するためには

SO

の移動という現象 を形式化する必要がある．

CCRN

ではこれをセグメ ントグラフと呼ばれる構造を用いて表現する．例とし て，図

4 (i)

では，

context c

^1と

c

^{2があり，それらの}

scope

は重なっている部分がある．ユーザは図

4 (i)

に 示したようなパス

αβ

に沿って移動できる．このよう な状況をセグメントグラフを用いて図

4 (ii)

のように 表現できる．ユーザはセグメントグラフ上を移動する ものとして，ユーザは常にセグメントグラフのいずれ かの頂点に位置するものとする．セグメントグラフの 各頂点にはその場所に存在する

context

の

scope

の集 合が対応づけされている．このようにして，図

4 (i)

のように

context

の

scope

に重なりがあったとしても 離散構造として表現できる．セグメントグラフは以下 のように定義される．

［定義

3

］（セグメントグラフ）

C

^を

context

の集合 とする．セグメントグラフ

G

^はタプル

( S, E, F )

であ る．ただし，

• S

はセグメントの有限集合

• E ⊆ S × S

は二つのセグメント間の有効辺であ り，

E

^{は左全域的である．（すなわち，}

∀s ∈ S, ∃s

∈ E s.t. ( s, s

) ∈ E

^）

• F : S → 2

^C はセグメントに対応する

context

の

scope

の集合が返る関数

図4 セグメントグラフの例 Fig. 4 Example of a segment graph.

である．

CCRN

は触媒反応ネットワークとセグメントグラ フの組合せで以下のように定義される．

［定義

4

］（

Context Catalytic Reaction Network

）

Context Catalytic Reaction Network (CCRN)

はタ プル

( O, C, R, G, L

^FIX

, l

⁰

)

である．ただし，

• O

^は

SO

の集合

• C

^は

context

の集合

• R

は触媒反応の集合（すなわち，触媒反応ネッ トワーク）

• G

^{はセグメントグラフ}

( S, E, F )

• L

^FIX

⊆ O × S

^{は固定された}

SO

の位置

• l

0

∈ S

^{は移動する}

SO

の初期に位置するセグメ ント（移動する

SO

は

O \ {o ∈ O | ∃s ∈ S. (( o, s ) ∈ L

FIX

) }

と表せる）

である．

3. 4

モデル検査

モデル検査は状態遷移系の性質を検証する手法で あり，産業的にも幅広い分野で使われている．モデル 検査では状態遷移系としてクリプキ構造

[11]

が用い られる．クリプキ構造の性質は様相論理と呼ばれる 論理によって記述される．様相論理は主に計算木論 理

(computational tree logic, CTL)

と線形時相論理

(linear temporal logic, LTL)

の二つが用いられるこ とが多いが，本論文では，後述の記号モデル検査では

CTL

を，有界モデル検査では

LTL

をクリプキ構造の 性質を記述する論理として用いる．

クリプキ構造は以下のように定義される．

［定義

5

］（クリプキ構造）

AP

^{を原子命題の集合とす} る．クリプキ構造

M

はタプル

( S, I, R, L )

で定義され る．ただし，

• S

^{は状態の有限集合}

• I ⊆ S

^{は初期状態}

• R ⊆ S × S

^{は遷移関係で，}

R

^{は左全域的であ} る（すなわち，

∀s ∈ S, ∃s

∈ S s.t. ( s, s

) ∈ R

）

• L : S → 2

^APはラベル関数 である．

次にクリプキ構造の性質を記述する論理として

CTL

と

LTL

の定義と意味論を挙げる．

CTL

は，並行プログラムの分析と設計の目的で

Clarke

らによって提案された

[12]

．

CTL

の文法は以 下のように定義される．

［定義

6

］（

CTL

文法）

AP

を原子命題の集合とする．

CTL

論理式

φ

は以下のような文法で再帰的に定義さ

れる．

φ ::= | ⊥ | p | ¬φ | φ ∨ φ |

EXφ | EGφ | EFφ | E ( φUφ ) | AXφ | AGφ | AFφ | A ( φUφ )

ただし，

p ∈ AP

．

右辺の項はそれぞれ，真，偽，原子命題

p

^{，否定，論} 理和のほか，

ne X t

，

G lobally

，

in the F uture

，

U ntil

という時相演算子，

Exists

，

All

という経路限定子 が含まれている．

CTL

の意味論は，クリプキ構造

M = ( S, I, R, L )

とその現在の状態

s ∈ S

^のペア

M, s

に関する充足の二項関係（本論文では

| =

の記 号を用いる）として定義される．以下に

CTL

の意味 論を列挙する．

• M, s | =

^{（真は常に満たす）}

• M, s | = ⊥

（偽は常に満たさない）

• ( M, s | = p ) iff ( p ∈ L ( s ))

（原子命題は現在の 状態のラベルに含まれているならば満たされる）

ブール的組合せの意味論は以下のとおりである．

• ( M, s | = ¬φ ) iff ( M, s | = φ )

• ( M, s | = φ ∨ ψ ) iff [( M, s | = φ ) ∨ ( M, s | = ψ )]

最後に，

CTL

の経路限定子と時相論理式の組合せの 意味論を列挙する．

• ( M, s | = EXφ ) iff

[ ∃s

∈ S. (( s, s

) ∈ R ∧ ( M, s

| = φ ))]

• ( M, s | = AXφ ) iff

[ ∀s

∈ S. (( s, s

) ∈ R ∧ ( M, s

| = φ ))]

• ( M, s | = EGφ ) iff s

から

R

による無限長の遷 移経路

s

⁰

, s

¹

, s

²

, . . .

^{が存在して，任意の}

k ≥ 0

に対 して

M, s

k

| = φ

^．

• ( M, s | = AGφ ) iff s

^から

R

^{で到達可能な任意} の

s

∈ S

^で

M, s

| = φ

^．

• ( M, s | = EFφ ) iff s

から

R

で到達可能な

s

∈ S

が存在して

M, s

| = φ

^．

• ( M, s | = AFφ ) iff s

^から

R

^{による無限長の任} 意の遷移経路

s

0

, s

1

, s

2

, . . .

^{に対して，ある}

k ≥ 0

に 対して

M, s

k

| = φ

．

• ( M, s | = E ( φUψ )) iff s

か ら

R

に よ る 無 限 長 の 遷 移 経 路

s

⁰

, s

¹

, s

²

, . . .

が 存 在 し て ，

[( ∃i. ( M, s

i

| = ψ )) ∧ ( ∀j < i. ( M, s

j

| = φ ))]

．

• ( M, s | = A ( φUψ )) iff s

^{か ら}

R

^{に よ る 無} 限 長 の 任 意 の 遷 移 経 路

s

0

, s

1

, s

2

, . . .

^{に 対 し て ，}

[( ∃i. ( M, s

i

| = ψ )) ∧ ( ∀j < i. ( M, s

j

| = φ ))]

．

LTL

は，計算機プログラムの形式的検証の目的で

Amir Pnueli

によって提案された

[13]

．

LTL

の文法は 以下のように定義される．

［定義

7

］（

LTL

文法）

AP

を原子命題の集合とする．

LTL

論理式

φ

は以下のような文法で再帰的に定義さ れる．

φ ::= | ⊥ | p | ¬φ | φ∨φ | X φ | G φ | F φ | φ U φ

ただし，

p ∈ AP

．

右辺の項は

CTL

のものと対応する項が含まれている が，

CTL

と異なり経路限定子は含まれない．次に，ク リプキ構造

M

^{における遷移パス}

π

^{を以下のように定} 義する．

［定義

8

］（遷移パス）

M

をクリプキ構造とする．

π = ( π

⁰

, π

¹

, π

²

, . . . )

は 無 限 長 の 遷 移 パ ス で あ り，

∀i. ( π

i

, π

i+1

) ∈ R

^{を満たす．また，}

π

^{i は}

π

^の

i

^番 目以降のサフィックスを指すものとする．すなわち，

π

ⁱ

= ( π

i

, π

i+1

, π

i+2

, . . . )

である．

LTL

の意味論は，クリプキ構造と遷移パスのペア

M, π

に関する充足の二項関係として定義される．以 下に

LTL

の意味論を列挙する．

• M, π | =

^{（真は常に満たす）}

• M, π | = ⊥

（偽は常に満たさない）

• ( M, π | = p ) iff ( p ∈ L ( π

0

))

（原子命題は遷移パ スの先頭のラベルに含まれているならば満たされる）

また，ブール的組合せの意味論は以下のとおりである．

• ( M, π | = ¬φ ) iff ( M, π | = φ )

• ( M, π | = φ ∨ ψ ) iff [( M, π | = φ ) ∨ ( M, π | = ψ )]

最後に，

LTL

の時相演算子の意味論を列挙する．

• ( M, π | = X φ ) iff ( M, π

¹

| = φ )

• ( M, π | = F φ ) iff

∃i. ( M, π

ⁱ

| = φ )

• ( M, π | = G φ ) iff

∀i. ( M, π

ⁱ

| = φ )

• ( M, π | = φ U ψ ) iff

( ∃i. ( M, π

ⁱ

| = ψ )) ∧ ( ∀j < i. ( M, π

^j

| = φ ))

モデル検査問題は，直感的には，あるクリプキ構造

M

が与えられた様相論理式

φ

^{を満たすかどうかを判} 定する判定問題である．モデル検査問題は与える様相 論理式が

CTL

か

LTL

かで問題が異なり，それぞれ以 下のように形式的に定義される．

［定義

9

］（

CTL

におけるモデル検査問題）

CTL

論理 式

φ

で記述された要求された性質とクリプキ構造

M = ( S, I, R, L )

が与えられたとき，モデル検査問題 は初期状態

s ∈ I

^の

M

^が，

M, s | = φ

^{を満たすかどう} かを判定する判定問題である．

［定義

10

］（

LTL

におけるモデル検査問題）

LTL

論 理式

φ

で記述された要求された性質とクリプキ構 造

M = ( S, I, R, L )

が与えられたとき，モデル検査問 題は初期状態

π

0

∈ I

^{から始まる遷移パス}

π

^{について，}

∀π. ( M, π | = φ )

を満たすかどうかを判定する判定問題 である．

モデル検査問題はクリプキ構造

M

^{の状態数が有限の場} 合はグラフ探索問題に帰着できることが知られている．

モデル検査問題を解くモデル検査器の実装に，

SPIN ( S imple P romela IN terpreter) [14]

などがある．

3. 5

記号モデル検査

モデル検査問題はクリプキ構造

M

^{の状態数が有限} の場合はグラフ探索問題に帰着できることが知られ ているが，大規模なクリプキ構造に対してモデル検査 すなわちグラフ探索を行うのはコストがかかる．そこ で，クリプキ構造に含まれる全状態や遷移関係を明示 的に保持せず，これらをブール関数で表現し，これを 二分決定グラフ

(BDD)

でコンパクトに格納したもの を用いて大規模な状態遷移系を効率的にモデル検査を 行う記号モデル検査が

McMillan

らによって提案され た

[4]

．記号モデル検査では，任意の状態集合

S

^を変 数ベクトル

θ

を用いて以下のブール関数

S (θ)

で表現 する．

S ( θ ) =

True θ ∈ S False otherwise

なお，「

θ

のある成分が特定の値である」ことを原子 命題とみなすことができる．

S ( θ )

を用いて初期状態

I ⊆ S

を表すブール関数も同様に

I ( θ )

として表現で きる．更に，状態

θ ∈ S

^から

θ

∈ S

^{への遷移関係}

R ⊆ S × S

を以下のブール関数

T ( θ, θ

)

として表現 する．

T (θ, θ

) =

True ( θ, θ

) ∈ R False otherwise

これらは実際に記号モデル検査を行う検査器の内部 では

BDD

として保持されているが，記号モデル検査 問題に帰着させるには

BDD

を直接検査器に与える必 要はなく，状態を表す変数ベクトル

θ

^，

S ( θ )

，

I ( θ )

，

T ( θ, θ

)

をブール関数として与えればよい．記号モデ ル検査を行う実装として，

NuSMV2 ( New S ymbolic

M odel V erifier version 2 ) [15]

が有名である．

3. 6

有界モデル検査

前節の記号モデル検査で導入した変数ベクトル

θ

と ブール関数

I ( θ )

と

T ( θ, θ

)

を用いて有界モデル検査 と呼ばれる手法を導入することができる．有界モデ ル検査は

Biere

らによって提案された手法であり

[5]

， 最も特徴的な点はモデル検査問題を充足可能性問題

(SAT)

に帰着する点である．充足可能性問題は

SAT

ソルバーによって解くことが多く，近年は，より大規 模な充足可能性問題を解くことができる

SAT

ソルバー が日々開発されてきている

[16]

．有界モデル検査は以 下のブール関数が充足するかどうかを判定する．

I ( θ

0

) ∧

_k−1

i=0

T ( θ

i

, θ

i+1

) ∧ ¬p ( θ

0

, . . . , θ

k

)

ただし，ブール関数

p (θ

0

, . . . , θ

k

)

はモデルの性質を 表す

LTL

式

φ

から有界モデル検査手法によって生成 される．また，

k

はモデルの初期状態から性質

φ

^を検 証するステップ数である．ステップ数が

k

^{に限定され} ているために，この手法は「有界」モデル検査と呼ば れている．もし上記のブール関数が充足するならば，

そのときの変数の割り当て

θ

0

, . . . , θ

kが

φ

^の反例に 対応する．そうでない場合，それは初期状態から少な くとも

k

^{ステップの範囲では}

φ

^{の反例が存在しないこ} とを意味する．近年開発された

SAT

ソルバーの多く は与えられたブール関数が仮に充足するとすればその 変数の割り当てを探すことの方が，どのような変数の 割り当てをしても充足しないブール関数を与えられた 場合に充足しないと判定することよりも得意である．

これは，有界モデル検査は

LTL

式で記述された与え られたモデルの性質の反例を検出すること用途に適し ていることを意味する．

NuSMV2

では

BDD

を用い た記号モデル検査と同じモデル検査問題を入力として，

この有界モデル検査も行うことができる．

4. CCRN

の記号モデル検査による検証 本節では，

CCRN

を記号モデル検査の問題に帰 着する手法を提案する．より具体的には，与えられ る

CCRN

から変数ベクトル

θ

，全状態を表す関数

S ( θ )

，初期状態を表す関数

I ( θ )

，遷移関係を表す関数

T (θ, θ

)

を作る方法を示す．これらをモデル検査を行 う

NuSMV2

へは，ほとんど直接的に

smv

^{ファイルと} して簡潔に記述し入力として与えることができる

[17]

．

CCRN ( O, C, R, ( S, E, F ) , L

FIX

, l

0

)

で保持される状 態には，

L

FIXで特定のセグメントに固定されておら

ず，ユーザが持ち運ぶ

SO O

^MOB

= O \ {o ∈ O |

∃s ∈ S. (( o, s ) ∈ L

^FIX

}

がどのセグメント

s ∈ S

^に 位置するかという状態と，

2

^|O|

− 1

通りのフェデレー ション

o

f が存在するか否かという状態の

2

種類があ る．前者は

|S|

の状態数があり，後者は

2

^2|O|−1の状 態数があり，仮に明示的に全状態数を数え上げると

|S| × 2

^2|O|−1という膨大な状態数になる．まず記号モ デル検査の問題に帰着させるための最初のステップと して状態を表す変数ベクトル

θ

^{を定義する．先の議論} から，

O

MOBがセグメント

s ∈ S

に位置する状態を

「

segment = s

」と表現し，フェデレーション

o

f が存 在する状態を「

fed( o

f

) = True

」と表現する．これら を用いて状態ベクトル

θ

^を

θ = (segment , fed( o

f

) , fed( o

f

) , · · ·

2^|O|−1

)

と 定 義 す る こ と が で き る ．ま た ，プ ラ イ ム 記 号 付 き の 状 態 ベ ク ト ル 表 記

θ

^{は ，}

θ

= (segment

, fed

( o

f

) , fed

( o

f

) , · · · )

を表すものとする．全状態集 合を表す

S ( θ )

は本論文では任意の

θ

について

True

であるようなブール関数とし，

T (θ, θ

)

で制約を設け るアプローチをとる．

始めにユーザは

l

0に位置しており，

SO

同士はフェ デレーションをしていない，つまり，

|o

f

| > 1

のフェ デレーションは存在しない，という初期状態

I ( θ )

を 以下のように表現する．

I ( θ ) = (segment = l

0

)

∧

⎛

⎝

of∈2O\{},|of|=1

fed( o

f

) = True

⎞

⎠

∧

⎛

⎝

o_f∈2O\{},|o_f|>1

fed( o

f

) = False

⎞

⎠

次に，

T ( θ, θ

)

を定義することを考える．定義を簡便 な表現にするため，幾つかの補助変数を定義する．ま ず，セグメントグラフ上のあるセグメント

s

^からエッ ジ

e

^{を辿り別のセグメント}

s

^へ

SO O

MOBが移動す る遷移を

S

e

(segment = s ) ∧ (segment

= s

)

と定義する．触媒反応による

SO

のフェデレーション の存在状態の変化に関する遷移も考える．まず，触媒

反応が一切起こらなかった場合の遷移を

R

∅

o_f∈2^O\{}

fed( o

f

) = fed

( o

f

)

更に，触媒反応

r = ( c, M, N )

が起こった際に

SO

の フェデレーションの存在状態が変化する遷移を

R

r

of∈N

fed

( o

f

) = True

∧

of∈M

fed

( o

f

) = False

∧

of∈(2^O\{})\(M∪N)

fed( o

f

) = fed

( o

f

)

と定義し，触媒反応

r

が起こるフェデレーションの状 態の条件を

RC

_r

of∈M

(fed( o

f

) = True)

と定義する．次に，セグメントグラフ上のセグメント

s ∈ S

^から

s

∈ S

^へエッジ

e

^{を辿って移動した際に} 反応する触媒反応の集合

R

appは以下のように与えら れる．

Rapp(e){(c, M, N)∈R|c∈F(s), O(c)⊇M}

ただし

O ( c ∈ C )

は，ユーザが持ち運ぶ

SO

と，

con- text c

のスコープの範囲内のセグメントに位置する固 定された

SO

の和集合であり，

O(c∈C) =OMOB∪ {o∈O| ∃s∈S.(c∈F(s),(o, s)∈LFIX)}

である．更に，セグメントグラフの各エッジ

e ∈ E

^に ついての遷移関係について

• R

app

( e ) = ∅

^{のときは，エッジ}

e

^{に沿ってユー} ザが移動をしても反応する触媒反応がないので，ユー ザが移動する遷移とその際に触媒反応が一切起こらな い遷移の連節で表現し，

• R

^app

( e ) = ∅

^{のときは，エッジ}

e

^{に沿ってユーザ} が移動した場合に反応する触媒反応があるので，「ユー ザが移動する遷移の際に，触媒反応の起こる条件を満 たしたならば，その触媒反応が起こる遷移を伴う」と いうことを連言で表現し，それが

R

^app

( e )

に含まれる 触媒反応のいずれかで起こることから，連言節の選言 で表現される．ただし，エッジ

e

^{に沿ってユーザが移} 動した場合に反応する触媒反応があったとしても，い ずれの触媒反応の起こるフェデレーションの条件も満

たさない場合があるので，その場合については触媒反 応が一切起こらない遷移も追加する

ということを考慮し，これを以下のような論理式で定 義する．

T

e

⎧ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎨

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎪ ⎪

⎩

S

e

∧ R

∅

R

app

( e ) = ∅

r∈R_app(e)

S

e

∧ RC

r

∧ R

r

∨

⎛

⎝ _S

_e

_{∧ ¬}

r∈R_app(e)

RC

r

∧ R

_∅

⎞

⎠ otherwise

これらを用いて

T (θ, θ

)

は以下のように定義する．

T ( θ, θ

) =

e∈E

T

e

5.

^{実験と評価}

5. 1

記号モデル検査によるスケーラビリティの実 験的評価

本節では，スケーラビリティの評価実験の結果を報 告する．本実験では，図

5

で表される

CCRN

で記述 された

UC

シナリオを検証対象とした．このシナリオ は

n

^{階建ての博物館の}

UC

シナリオであり，各階に廊 下と展示室が

1

部屋ある．博物館の入り口と出口には ユーザの電話とヘッドセットが音声ガイドとしての役 割を果たすための触媒反応に対応する

context c

^1と

c

2がある．各展示室

i

^{には展示物}

d

^{(i)があり，}

d

^(i)に 対応する説明をユーザが受けるための触媒反応に対応 する

context c

⁽3ⁱ⁾と

c

⁽4ⁱ⁾がある．セグメントグラフ中 の有向辺

( s

⁽6ⁱ⁾

, s

⁽2ⁱ⁺¹⁾

)

と

( s

⁽6ⁱ⁺¹⁾

, s

⁽2ⁱ⁾

)

は各階の間の階 段に対応する．このような

UC

シナリオで

n

^の大きさ を変えながら，以下の

CTL

式を満たすかどうかの検 証を行う．

AG(segment = s

⁽¹⁾1

→AF(segment= s

⁽4ⁿ⁾

→ fed({a, b, d

⁽ⁿ⁾

}) = True))

この

CTL

式の直感的な意味は，ユーザが博物館の入 り口に入ったならば，最上階の展示室の展示物の説明 を受けることが常にできるという意味である．実験に は

CPU

が

Core i7 3820QM

，主記憶

16GB

の計算機 を用い，モデル検査器は

-AG

オプションを有効化した

NuSMV Version 2.6.0

を用い，素朴な手法

[3]

と本論

図5 実験で用いたCCRNで記述されたUCシナリオ Fig. 5 CCRN of a UC scenario used in experiments.

表1 スケーラビリティの評価実験結果

Table 1 Results of a Experiment of scalability evaluation.

実験インスタンス 素朴な手法[3] 提案手法 n |O| |C| |S| CPU (s) MEM (MB) CPU (s) MEM (MB)

1 4 4 6 0.01 12.06 0.01 12.48

2 5 6 11 0.01 13.50 0.01 13.67

3 6 8 16 0.24 37.05 0.01 16.35

4 7 10 21 5.45 566.57 0.02 24.11

5 8 12 26 172.30 12,528.02 0.08 47.68

6 9 14 31 N/A MEM. Out 0.37 127.97

7 10 16 36 — — 1.47 425.63

8 11 18 41 — — 5.75 1,546.30

9 12 20 46 — — 57.30 6,113.32

10 13 22 51 — — 264.26 11,309.29

11 14 24 56 — — N/A MEM. Out

備考 「MEM. Out」は計算機の主記憶不足で実験を中断したことを示す．

図6 CCRNの欠陥検出に要する計算コスト Fig. 6 Computational costs for CCRN

fault detection.

文の提案手法を比較した．素朴な手法では，

CCRN

を モデル検査の問題に帰着させる際に全ての状態を明示 的に記述するエンコーディングを行っているため，た

とえ

NuSMV2

を用いていたとしても記号モデル検査

の利点はほとんど生かせていない手法である．実験結 果は表

1

のとおりである．表の左側が実験インスタン ス，表の右側はそれを検証するのに要した

CPU

時間 と使用主記憶量である．この実験環境では，素朴な手 法を用いると

5

階の博物館のインスタンスで主記憶の 制約から限界に達しているが，提案手法では

10

階の 博物館のインスタンスまで同様の環境で検証すること が可能になった．この結果から，記号モデル検査を用 いることで，より多様な

UC

シナリオの検証が現実的 な計算コストで行えるようになったといえる．

5. 2

有界モデル検査による反例検出の実験的評価 本節では，有界モデル検査の有用性を示すための実 験の結果を報告する．この実験では，図

5

で示すよう な前節で用いた

CCRN

と同じものを用いるが，反例

検出の目的で図

5

の

CCRN

からランダムに触媒反応

c

⁽3ⁱ⁾と

c

⁽4ⁱ⁾を意図的に取り除いたものとする．この方 法で，同一部屋数の

CCRN

を

10

インスタンスを生 成し，部屋数

n = 1

から

n = 10

の範囲で合計

100

インスタンスの「設計に問題のある箇所が含まれた」

CCRN

から反例検出を有界モデル検査で行う．本実験 では，以下の

LTL

式で表現された性質を満たすか検 証を行う．

G

n i=1

(¬(segment = s

⁽4ⁱ⁾

)

∧ fed( {a, b, d

⁽ⁱ⁾

} ) = False)

∨ (segment = s

⁽4ⁱ⁾

∧ fed( {a, b, d

⁽ⁱ⁾

} ) = True)

この

LTL

式の直感的な意味は，「各部屋の展示物に対 応する解説のための触媒反応が全ての部屋で起こる」

ということである．本実験に用いた計算機やモデル検

査器は前節の実験で用いたものと同一である．また有 界モデル検査を行うにあたって，検証を行う状態数の 範囲

k

^{は初期状態から}

50

ステップの

k = 50

とした．

実験結果を図

6

と図

7

に示す．図

6

のプロットの各点 の色は実験インスタンスの大きさ，すなわち，博物館 の階数に対応しており，各点の座標は欠陥を検出する のに要した計算コストを表している^（注1）．この結果か らは，

n = 10

であるような大きな実験インスタンス であっても場合によっては

10

秒台で欠陥検出が行え ていることが分かる．より詳細に欠陥検出のためのモ デル検査に要した時間を記号モデル検査と有界モデル 検査の

2

手法で比較したプロットが図

7

である．ただ し，記号モデル検査では，上記

LTL

式と同等の意味 となる以下の

CTL

式で検証を行っている．

AG

n i=1

( ¬ (segment = s

⁽ⁱ⁾4

)

∧ fed( {a, b, d

⁽ⁱ⁾

} ) = False)

∨ (segment = s

⁽4ⁱ⁾

∧ fed( {a, b, d

⁽ⁱ⁾

} ) = True)

このプロットの各点は実験インスタンスであり，各点 の色は図

6

と同様に実験インスタンスの大きさに対応 し，横軸は有界モデル検査で検証に要した時間，縦軸 は記号モデル検査で検証に要した時間である．このプ ロットの点線よりも上側に点がプロットされているな らば，それは記号モデル検査よりも有界モデル検査の 方が高速に検証が行えたことを意味する．このプロッ トからもほとんどの場合で有界モデル検査を用いる方 が高速に欠陥検出が行うことができており，最大で

10

倍程度高速であることが分かる．図

6

のプロットで赤 丸で囲った

n = 1

の実験インスタンスは，他の

n = 1

の実験インスタンスに比べて検証に時間を要している．

また，図

7

のプロットで赤丸で囲った実験インスタン スは，図

6

のプロットで赤丸で囲った実験インスタン スに対応しており，これらの実験インスタンスは，記 号モデル検査で検証を行うよりも時間を要しているこ とも分かる．これは，これらの実験インスタンスでは どの触媒反応も取り除かれず，偶然欠陥がない実験イ ンスタンスになっていたことに起因する．有界モデル

（注1）：本実験で用いた全ての実験インスタンスにおいて，欠陥検出後 に反例作成に要した時間はいずれも0.01秒以下であり，欠陥検出まで の時間が支配的であった．これは後述の比較実験の図7の結果におい て，記号モデル検査を用いた場合についても同様であった．

図7 記号モデル検査(SMV)と有界モデル検査(BMC) によるCCRNの欠陥検出に要する時間の比較 Fig. 7 Fault detection time comparison between

symbolic model checking and bounded model checking.

検査を行う検査器では性質を満たすかどうかを帰納的 に検証（本実験の場合では，

k = 1

から

k = 50

まで を逐次的に検証）していき，性質を満たさない反例を 見つけ次第，検証を終了し反例を出力する．しかし，

上で挙げたような欠陥がない実験インスタンスを有界 モデル検査で検証しようとすると検査器は，本実験の 設定の場合，

k = 50

までの範囲を帰納的に検証するこ とを強いられる．有界モデル検査では，

k

^{を増加させ} るたびに，実験インスタンスに対応する

SAT

問題を 生成する必要があり，更に，この

SAT

問題は

k

^が大 きくなるほど問題規模が大きくなるため，

SAT

問題生 成や

SAT

問題を解くために計算コストがかかる．こ の結果，このような実験インスタンスにおける

CPU

時間やメモリ使用量が増大に繋がる．逆に，検証しよ うとする

CCRN

に欠陥があれば有界モデル検査はそ れを高速に検出できるといえる．

6.

^{む す び}

本論文では，

CCRN

で記述された

UC

シナリオを 記号モデル検査を用いて効率的に検証するための帰着 手法を提案した．これにより，素朴な手法

[3]

よりも大 規模な

UC

シナリオの検証が現実的な計算コストで行 えることをケーススタディとして実験的に示した．更 に，有界モデル検査が特に

UC

シナリオの欠陥検出へ の有用なアプローチであることも示した．しかしなが ら，状態を表す変数ベクトルの定義の方法に工夫をす るなどの

UC

シナリオの検証手法のスケーラビリティ に関する改善の余地が残っており，今後の課題として 引き続き取り組む予定である．

謝 辞 本 研 究 の 一 部 は

JSPS

科 研 費 基 盤

(S) 15H05711

の助成による．

文 献

[1] Y. Tanaka, “Proximity-based federation of smart ob- jects: liberating ubiquitous computing from stereo- typed application scenarios,” in Knowledge-Based and Intelligent Information and Engineering Systems, pp.14–30, Springer, 2010.

[2] J. Julia and Y. Tanaka, “Proximity-based federation of smart objects,” J. Intelligent Information Systems, vol.46, no.1, pp.147–178, Feb. 2016.

[3] R. Minoda, Y. Tanaka, and S. Minato, “Verifying scenarios of proximity-based federation among smart objects through model checking,” Proc. UBICOMM 2016 The Tenth International Conference on Mobile Ubiquitous Computing, Systems, Services and Tech- nologies, no.c, pp.65–71, 2016.

[4] K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.

[5] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Sym- bolic model checking without BDDs,” Tools and Al- gorithms for the Analysis and Constructions of Sys- tems, no.97, pp.193–207, 1999.

[6] R. Minoda and S. Minato, “Efficient scenario verifi- cation of proximity-based federations among smart objects through symbolic model checking,” Proc.

2nd International Conference on Pervasive Embed- ded Computing, pp.13–21, 2017.

[7] P. Herber, M. Pockrandt, and S. Glesner, “STATE – A SystemC to timed automata transformation en- gine,” 2015 IEEE 17th International Conference on High Performance Computing and Communications, 2015 IEEE 7th International Symposium on Cy- berspace Safety and Security, and 2015 IEEE 12th International Conference on Embedded Software and Systems, pp.1074–1077, 2015.

[8] Y. Sun, T.-Y. Wu, X. Li, and M. Guizani, “A Rule Verification System for Smart Buildings,” IEEE Trans. Emerging Topics in Computing, vol.5, no.3, pp.367–379, July 2017.

[9] C. Xu and S.C. Cheung, “Inconsistency detection and resolution for context-aware middleware support,”

Proc. 10th European Software Engineering Confer- ence Held Jointly with 13th ACM SIGSOFT Inter- national Symposium on Foundations of Software En- gineering, pp.336–345, 2005.

[10] S. Kauffman, Investigations, Oxford University Press, Oxford, New York, 2002.

[11] S.A. Kripke, “Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi,” Zeitschrift f¨ur Mathematische Logik und Grundlagen der Math- ematik, vol.9, no.5-6, pp.67–96, 1963.

[12] E.M. Clarke and E.A. Emerson, “Design and syn- thesis of synchronization skeletons using branching

time temporal logic,” pp.52–71, Springer Berlin Hei- delberg, Berlin, Heidelberg, 1982.

[13] A. Pnueli, “The temporal logic of programs,” 18th Annual Symposium on Foundations of Computer Sci- ence (SFCS 1977), pp.46–57, 1977.

[14] G.J. Holzmann, “The model checker SPIN,” IEEE Trans. Softw. Eng., vol.23, no.5, pp.279–295, May 1997.

[15] A. Cimatti, E. Clarke, and E. Giunchiglia, “Nusmv 2: An opensource tool for symbolic model checking,”

Computer Aided Verification, vol.2404, pp.359–364, 2002.

[16] M. Jarvisalo, D. Le Berre, O. Roussel, and L. Simon,

“The international SAT solver competitions,” AI Magazine, vol.33, no.1, pp.89–94, 2012.

[17] R. Cavada, A. Cimatti, C.A. Jochim, G. Keighren, E. Olivetti, M. Pistore, M. Roveri, and A. Tchalt- sev, “NuSMV 2.6 User Manual,” 2016. 2017年6月7 日閲覧．http://nusmv.fbk.eu/NuSMV/userman/v26/

nusmv.pdf

（平成29年6月8日受付，10月3日再受付，

12月4日早期公開）

蓑田玲緒奈 （学生員）

北海道大学大学院情報科学研究科博士後 期課程在学．2010北海道大学工学部情報 エレクトロニクス学科卒．2012同大学院情 報科学研究科修士課程了．2014から2016 までJST ERATO湊離散構造処理系プロ ジェクトにて研究補助員として従事．2016 より科研費基盤(S)離散構造処理系プロジェクトにて研究補助 員として従事．

湊 真一 （正員：シニア会員）

北海道大学大学院情報科学研究科教授．

1988京都大学工学部情報工学科卒．1990 同大学院修士課程，1995同博士課程（社会 人）了．博士（工学）．1990〜2004 NTT 研究所に勤務．1997スタンフォード大学客 員研究員（兼務），2004北海道大学助教授．

2010同教授（現職）．2009〜2015科学技術振興機構(JST)

ERATO湊離散構造処理系プロジェクト研究総括を兼務．大規

模離散構造データの表現と演算処理アルゴリズムの研究教育に 従事．著書に“Binary Decision Diagrams and Applications for VLSICAD”（Kluwer, 1995年）など．情報処理学会シニ ア会員，人工知能学会，IEEE各会員．