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

情報制御システムのモデル検査におけるモデル分割支援法の検討
古木 隆裕

小飼 敬

上田 賀一

モデル検査は，検査対象となるシステムの動作を抽象的に記述した振舞いモデルから状態遷移モデルを作成し，その状態遷移モデルの網羅探索を行う手法である．モデル検査を適用するシステムの規模によっては，探索すべき範囲が爆発的に増大するため，網羅探索が終わらなくなる問題 (状態爆発) が発生する．先行研究において，振舞いモデルを複数のモデルに分割し，探索すべき範囲を縮小することで状態爆発に対処する手法を提案したが，モデルの分割処理は手作業で行われるため，この手法の効果は適用者が持つ経験や知見に依存するものであった．そこで本研究では，先行研究における振舞いモデルの分割処理を，経験や知見に依らず，振舞モデルの特性から手順的に行うための手法を検討した．評価実験の結果，提案した手順に従うことで，振舞いモデルを複数のモデルに分割できることを確認した．

Model checking is a method that makes state transition model from the behavior model of target system andsearches it exhaustively. Depending on target systems scale, the range that need to search becomes wide
explosively, and in this case, exhaustive search takes too long time to finish (called ”state-explosion”).Our
previous study shown a method that avoid the state-explosion by reducing search range using divided behavior models (the partial behavior model against the entire behavior model), but its eﬀects depend on user’s
knowledge and experience of the dividing method. This study proposes a method to divide the behavior
model procedurally by using properties of non-divided behavior model, without knowledge and experiencefor dividing model. Evaluation experiment results show that the proposed method can procedurally divide
the behavior model.

は，実施するシステムの規模が増大するにつれ，網羅1 はじめに探索すべき状態の個数が爆発的に増加する現象があ大規模なシステムは不具合発生時に与える社会的り，これを状態爆発と呼ぶ．モデル検査において状態影響が大きいため，高い信頼性が求められる．そのよ爆発が発生した場合，網羅探索に膨大な時間が必要とうなシステムの信頼性を確保する手段の一つに，形式なったり，網羅探索の実行時にメモリ容量が足りなく手法の一種であるモデル検査が挙げられる．

なるため，結果としてモデル検査を完了できなくなる

モデル検査は，主にシステム開発の上流工程において用いられる検証技術であり，検査対象となるシステ[6]．このため，モデル検査に際しては往々にして状態爆発への対策が求められる．

ムの動作を抽象的に記述した振舞いモデルから状態本研究の先行研究において，状態爆発への対策とし遷移モデルを作成し，その状態遷移モデル内の状態のて段階的検査法 [5]，および段階的検査法を用いたモ網羅探索を通して，不具合 (システムが取るべきでなジュラ検証 [7] を提案した．モジュラ検証では，振舞い状態) を引き起こす動作を発見する．モデル検査にいモデルを複数の部分に分割することで，作成されるModel division support method in model checking of
information control systems
Takahiro Furuki， Yoshikazu Ueda, 茨城大学, Ibaraki
University.
Kei Kogai, 茨城工業高等専門学校, Ibaraki National
College of Technology.

状態遷移モデルの大きさを縮小させ，網羅探索する範囲を削減することで状態爆発に対処する．このとき，振舞いモデルの分割処理は手法の適用者により手作業で行われるため，効果の大きい分割処理を行えるかどうかは，適用者が持つ経験や知見に依存する．

ルで表現された制御ルールに従い変化させることを状態遷移と呼び，振舞いモデルにおいて起こりうる全ての状態遷移からなる集合を状態遷移モデルと呼ぶ．
また，振舞いモデルが取り得る全ての状態からなる集合を状態空間と呼ぶ．モデル検査においては，振舞いモデルと検査項目をモデル検査器に対する入力とし，モデル検査器の内部で振舞いモデルを基に状態遷移
図1

情報制御システム

本研究では，モジュラ検証における分割処理を，適用者の経験や知見に依存せずに実行する手法を提案する．

モデルを生成して，これに対して網羅探索を行う．

2. 3 段階的検査法
段階的検査法は，モデル検査における状態爆発を回避するための手法である．段階的検査法は，以下の 2つの考え方に基づく．

2 関連知識1. 状態空間分割

2. 1 情報制御システム

状態空間を複数のより小さな部分に分割し，各々情報制御システムとは，本来作業員が手作業で行っに対してモデル検査を適用することで，一度に探ていたシステムの操作について，その手順やノウハ索する範囲を縮小させ，状態爆発を回避する．

ウをルール化することで，そのルールに基づいた設

2. 属性着目

備の自動制御を実現するシステムである．社会にお検査項目と関係しない属性は検査に影響を与えいては，列車の運行管理や電力制御といったインフラない [2] ことを利用し，振舞いモデルからそれに系のシステムや，工場のライン制御などの産業系の該当する属性や制御ルールを除くことで，生成さシステムに利用されている．情報制御システムは，制れる状態遷移モデルを縮小させ，状態爆発を回避

御プログラムと物理環境の 2 部分より構成される (図する．

1)．情報制御システムは制御プログラムを中心に駆動

段階的検査法の処理は 1 次処理と 2 次処理に分かし，センサを介した物理環境情報の非同期な取得，物れ，1 次処理では属性着目による状態空間の縮小と，理環境情報の仮想環境への反映，仮想環境情報とルー

その状態空間を基とした状態遷移モデルの作成を行

ルに基づく次の操作方法の判断および操作指示といっう．2 次処理では，生成された各状態遷移を結合したた手順を任意の周期で繰り返し実行する．

のち，網羅探索を行う．モジュラ検証における振舞いモデルの分割に関連する 1 次処理について説明する．

2. 2 情報制御システムの振舞いモデル

1 次処理，および前処理の概念図を図 2 に示す．1

振舞いモデルとは，検査対象となるシステムの動作

次処理は，図 2 中の点線内の処理に相当する．初めを抽象化し，それを文字や図で表現したものである．に，振舞いモデルから検査項目に出現する属性のみを情報制御システムを振舞いモデルとして表現する場

抽出し，それらの属性の組からなる状態を全て導出し合，制御プログラムを制御ルールモデル，物理環境をて，着目状態集合とする．次に，着目状態集合から状物理環境モデルにそれぞれ対応付ける．振舞いモデ

態を一つ取り出し，状態マネージャへの入力とする．

ルは，自身の性質の種類 (属性) とその値 (属性値) を状態マネージャは，入力された状態に対し適用できる保持する．また，ある時点で振舞いモデルが保持して制御ルールを全て適用して，新たな状態を生成する．

いる属性値の組合せを，振舞いモデルの状態と呼び，最後に，この状態遷移を部分遷移とし，部分遷移モデ

特にシステムの開始時にシステムが取る状態を，初期ルとして記録する．これらの手順を全着目状態に対し状態と呼ぶ．振舞いモデルの状態を，制御ルールモデ実行することで，与えられた振舞いモデルの状態遷移図2

前処理・1 次処理の概念図

図4

情報制御システムの構成基となる情報制御システムと同じ振舞いを示す．同様に，サブシステムの振舞いモデル (つまり，モジュール) についても，その集合を以て基となる情報制御システムの振舞いモデルを表現できる．
ここで，モジュール間をまたぐ関係を相互関係と呼ぶ．相互関係は，物理的制約によるものと，制御ルールによるものがある．モジュラ検証において段階的検査法を適用した場合，2 次処理の際に，各モジュールの状態遷移モデルを相互関係を用いて接続し，モジュール分割前の振舞いモデルに対応する状態遷移モ
図3

モジュラ検証における分割デルを生成する必要がある．
本研究では，上記で述べた振舞いモデルの分割方モデルを得る．

法のうち，振舞い間の影響が小さい箇所を境とする分割 (以下，振舞い分割と呼ぶ) に注目する．振舞い

2. 4 モジュラ検証

分割においては，制御ルールによる相互関係を少な

本研究の対象とするモジュラ検証は，検査対象のシくする必要がある．ある 2 つのモジュールがある時，ステムの振舞いモデルを，物理的結合度が低い箇所，一方のモジュールのある制御ルールの適用結果が，他構造的対称性がある箇所，振舞い間の影響が小さい方のモジュールのある制御ルールの実行の可否に影箇所を境に複数部分に分割し，そのような分割によ響するとき，これら 2 つのモジュールの間には制御り生成された各振舞いモデル (以下，モジュールと呼ルールによる相互関係が 1 つ存在するといえる．制ぶ) について検証を行う手法である (図 3)．分割によ御ルールによる相互関係が多い場合，2 つのモジューり生成されたモジュールは，段階的検査法への入力とルがお互いに他方のモジュールの情報を多く使用しなる．ていることになる．つまり，分割後の各モジュールに情報制御システムは，そのサブシステムの集合とし他方の情報が多く含まれ，モジュールの重複部分が大ても表現でき，各サブシステムも情報制御システムときくなるため，分割の効果が小さくなる．また，モして扱う (図 4)．システムを構成する各サブシステム

ジュールの共通部分が大きくなると，2 次処理の結合が互いに情報をやり取りし協調して動作することで，におけるモジュール間の接続箇所が多くなるため，結果として処理時間が増加する．

2. 最小カットの導出
生成した無向グラフについて，その最小カットを3 提案手法求める．最小カットの導出にあたっては，永持・2.4 節で述べた通り，振舞い分割においては，制御茨木のアルゴリズム [4] を適用する．図 5 中央のルールによる相互関係を少なくする必要がある．

無向グラフにおいて，最小カットは r3 と r4 を接本研究における，制御ルールの定義を述べる．制御

続する辺である．この最小カットは，最も効果のルールは実行条件と実行結果の組から成り，それぞれ大きい振舞い分割が，制御ルール r1 ，r2 ，r3 を論理式で示される．実行条件および実行内容に含まれ含むモジュールと，制御ルール r4 ，r5 ，r6 を含る各命題は”属性名=属性値”の形で示され，左辺が示むモジュールへの分割であることを示している．

す振舞いモデルの属性が，右辺が示す属性値を持つ場(図 5 右 )合に真になる．図中では，制御ルールを(実行条件) ⇒ (実行内容)の形で示し，以降特に記述がない限り，制御ルールはこの形式で示す．振舞いモデルにおいては，制御ルー4 事例研究提案手法を情報制御システムの振舞いモデルに適用し，適用結果の確認と考察を行う．

ルの実行条件が満たされると，制御ルールが実行され，実行結果に示された属性の変化を振舞いモデルに

4. 1 適用対象のシステム反映する．つまり，制御ルール実行により変化する属

先行研究 [5] において用いられた，列車運行システ性が，他の制御ルールの実行条件に出現している場

ムを手法適用の対象とする．列車運行システムは，列合，その 2 つの制御ルール間に相互関係が存在する．

車の移動を自動制御するシステムであり，列車運行のここで，V を制御ルールの集合，E を制御ルール間安全性の確保を目的とする．の相互関係の集合とした無向グラフ G=(V，E) を考適用対象の列車運行システムの路線構成を図 6 にえる．G における辺の重みは，すべて 1 とする．こ示す．図 6 中において，太線で区切られた箇所を軌道のとき，振舞いモデルを 2 分割することを考慮する回路と呼ぶ．軌道回路には，列車が 1 台進入できる．と，制御ルールによる相互関係が最も少ない場所は，区別のため，各軌道回路を 1T，2T，．
，16T とし，図G の最小カットと一致する．したがって，G の最小6 のように対応付ける．図 6 の路線においては，列車カットにより分割された 2 つの頂点集合が示す制御の進行方向が右向き・左向きの 2 種類存在し，各軌道ルール群が，最も相互関係の少ない制御ルールの組で回路ごとに片方向，あるいは両方向への進行方向が定あり，それらを別々に含む 2 つのモジュールへの分割められている．以下に，進行方向と軌道回路の対応をが，全ての可能な振舞い分割の中で最も効果の大きい示す．

振舞い分割である．

右向き

提案手法は，以下の 2 つの処理で構成される．

1T，2T，3T，4T，6T，7T，8T，9T，11T，12T，

1. 無向グラフ生成

13T，14T

振舞い分割の対象となる振舞いモデルを参照し，左向きV を対象の制御ルールの集合，E を対象の制御2T，4T，5T，6T，7T，10T，9T，11T，12T，ルール間の相互関係の集合とした，無向グラフ

15T，14T，16T

G=(V，E) を作成する．図 5 の振舞いモデル (図4. 1. 1 振舞いモデル

5 左) に対し上記を適用した場合，無向グラフ (図手法適用にあたっては，便宜上，先行研究で用いら5 中央) が生成される．なお，制御ルール中に出れた振舞いモデルを簡略化し，列車の進行に関する制現する属性値や論理演算子は，生成される無向グ御ルールのみに注目した振舞いモデルを作成する．

ラフに影響を与えないため，すべて無視する．

列車の進行に関する制御ルールの概要図を図 7 に

図5

図6

提案手法の概要図

列車運行システムの路線構成する」と考え，各軌道回路とその在線状況を振舞いモデルの属性および属性値とし，制御ルールを以下のように表す．

1T = (列車が存在)∧

2T = (列車が不在)⇓
1T = (列車が不在)∧

2T = (列車が存在)

軌道回路 2T から軌道回路 3T への進行など，他の
図7

制御ルール「列車の進行」の概要

軌道回路の組も同様にして，上記の式の形で制御ルールを作成し，その制御ルールの集合から振舞いモデル示す．図 7 は，図 6 における軌道回路 1T から軌道回路 2T への列車の進行を表している．ここで，「軌道回路 1T から軌道回路 2T への移動」を「軌道回路1T 上の列車を無くし，軌道回路 2T 上に列車を配置を作成して，手法の適用対象とする．

4. 2 適用結果

1. 各モジュールの状態空間のサイズの大小

前節で定義した振舞いモデルに対し提案手法を適

2 つのモジュールの状態空間の大きさに大きな差用したところ，分割方法が 3 種類示された．各分割がある場合，状態空間の大きい方のモジュールか方法において得られた 2 つのモジュールのうち，片ら導出された状態遷移モデルに対して網羅探索方の制御ルールが示す列車の進行を図 6 に記したもを行う際に，状態爆発が発生する可能性がある．のを，それぞれ図 8，図 9，図 10 に示す．

そのため，2 つのモジュールの状態空間の大きさが均等であればあるほど，振舞い分割に適してい

4. 3 考察
適用結果として，振舞い分割方法が複数提示されるとみなす．

2. 各モジュール内の制御ルールの個数た．その原因は，本手法で得られる振舞い分割方法

制御ルールの個数は，そのモジュールから導出さが，モジュールの相互関係の個数のみを基準としていれる状態遷移モデルにおける，遷移の種類数に相るためである．今回適用対象とした情報制御システ

当する．つまり，制御ルールの個数が増加するにムの路線構成 (図 6) は，同じ形状の路線を 3 つ接続つれ，そのモジュールから導出される状態遷移モしたものである．つまり，軌道回路 1T〜6T，6T〜デルも大きくなり，同時に状態爆発発生の可能性

11T，および 11T〜16T の構成は同一である．

も高まる．状態空間と同様の考え方に基づき，2

ここで，軌道回路 1T〜6T に注目する．進行方向がつのモジュールの制御ルールの個数が均等であれ片方向である軌道回路は 3T，5T である．3T，5T にばあるほど，振舞い分割に適しているとみなす．

は片方向からしか進入できないため，1T，2T，4T，6T を実行内容に含む制御ルールに比べ，3T，5T を5 関連研究

実行条件・実行内容に含む制御ルールの個数は少な

L.Antuña らは，群ロボットシステムを対象にしたい．したがって，3T，5T に進行/脱出する制御ルー

モデル検査における状態爆発の対策手法について述

ル間の相互関係の個数が，軌道回路 1T〜6T におけべている [1]．手法は，群ロボットを誘導するアルゴる制御ルールの中で最も少なくなる．図 8 を見ると，リズムについて，群ロボットの動作をグリッドで管理振舞い分割後のモジュールにおいて，3T に進行するし，そのグリッド上で動作する群ロボットの振舞いの制御ルールと，3T から脱出する制御ルールが別々の対称性の利用や，グリッド上のロボットの座標の相対モジュールに存在することが分かる．5T についても化を通してルールを削減し，状態空間の削減を行うも同様の分割がなされている．のである．

同形状の 6T〜11T，および 11T〜16T についてもJ.F.Groote らは，システムの状態空間が大きくな同じ考え方が適用でき，それぞれ図 10，図 9 から同らないように仕様を作成するためのガイドラインを様の結論を見出せる．しかし，図 8，図 9 においては，提示した上で，その妥当性について述べている [3]．

2 つのモジュールが内包する属性と制御ルールの個数

これらの文献においては，適用対象のシステムの知に大きな差があることは明らかである．一方，図 10

識や，システムモデリングの経験に依存した手法を通に関しては，そのような差は他の 2 つの振舞い分割して，状態空間の削減がなされている．本研究で述べ方法よりも少ないと考えられる．

る手法は，既存の振舞いモデルに対し，そのような知これらの振舞い分割手法の間で異なる要素である，識や経験に依らず，規定の処理手順に沿って処理を実モジュール間の属性と制御ルールの個数に着目し，以行することで振舞い分割を行い，それにより状態空間下に示す基準を考案した．手法の適用により複数の振の削減を実現するものである．

舞い分割方法が提示された場合，これらの基準を適用することにより，提示された振舞い分割方法のさらなる絞り込みが可能になると考えられる．

図8

振舞いモデルの分割方法 1

図9振舞いモデルの分割方法 2

図 10

振舞いモデルの分割方法 3

う手法を述べた．分割処理を手順的に行うことで，適6 まとめ用者が持つ経験や知見に依らない処理を実施できる．

本研究では，情報制御システムを対象にモジュラ検今後は，物理的結合度や構造的対称性に着目した振舞証及び段階的検査法を適用する際に行う振舞いの分いモデル分割の支援法の検討や，複数の振舞い分割方割処理を，振舞いモデルの情報を用いつつ手順的に行法が提示された場合に，その絞り込みを行う手法の体系化および自動化を行う．
謝辞 本研究を進めるにあたり，丁寧かつ熱心なご指導を賜りました (株) 日立製作所の松本一人様，武澤隆之様，山形知行様，横浜研究所の秦野康生様に深く感謝致します．

参 考 文 献[1] Antuña, L., Araiza-Illan, D., Campos, S., andEder, K.: Symmetry Reduction Enables Model
Checking of More Complex Emergent Behavioursof Swarm Navigation Algorithms, Springer International Publishing, 2015, pp. 26–37.
[2] Clarke, E., Grumberg, O., and Peled, D.: Model
Checking, MIT Press, 1999.

[3] Groote, J. F., Kouters, T. W. D. M., and Osaiweran, A.: Specification Guidelines to Avoid theState Space Explosion Problem, Springer Berlin Heidelberg, 2012, pp. 112–127.
[4] Nagamochi, H. and Ibaraki, T.: A linear-timealgorithm for finding a sparsek-connected spanning subgraph of ak-connected graph, Algorithmica,Vol. 7, No. 1(1992), pp. 583–596.
[5] 小山恭平, 小飼敬, 上田賀一: 情報制御システムに対する SPIN を用いた段階的モデル検査手法, 日本ソフト
ウェア科学会大会論文集, Vol. 30(2013), pp. 274–281.
[6] 萩谷昌己, 吉岡信和, 青木利晃, 田原康之: SPIN による設計モデル検証 : モデル検査の実践ソフトウェア検証, トップエスイー実践講座 3, 近代科学社, 2008.
[7] 宮島卓巳, 小飼敬, 上田賀一, 山形知行, 武澤隆之: モ
ジュラ化手法によるモデル検査の検討とモジュラ検証の実用化, 電子情報通信学会技術研究報告. KBSE, 知能ソ
フトウェア工学, Vol. 114, No. 501(2015), pp. 25–30.