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

情報制御システムにおける段階的検査法を用いたモジュラ検証
宮島 卓巳

小飼 敬

上田 賀一

山形 知行

武澤 隆之

モデル検査は検査対象の振舞いモデルを機械的かつ網羅的に探索を行うことで，仕様通り振舞うか検査する手法である．しかし，実践的なモデルに対しモデル検査を適用する場合，状態爆発が発生する可能性が高い．本研究では，検査対象のシステムをいくつかのサブシステムに分割して検証するモジュラ検証を段階的検査法を用いて実現する．サブシステムごとに分割してモデル化を行い，それぞれ他モデルの状態を入力として与えながら段階的検査法を適用し，領域間の横断に加え，モデル間の横断を改めて繋ぐことでモデル検査を行う．これにより検証モデル内の状態数を削減でき，状態空間の肥大化を防ぐことができる．本研究では，列車運行システムにおいて段階的手法のみ適用の場合とモジュラ検証した場合の比較を行い，有効性を評価する．

Model checking is a veriﬁcation method that veriﬁes mechanically and comprehensively the behavioral modelof target system to check behavior of the speciﬁcation. However, state explosion is more likely to occur
when applying model checking to the practical system. In this study, we realize the modular veriﬁcationthat veriﬁes of some subsystems that divide system using a stepwise model checking method. This method
is combining crossing state space and crossing models after that every subsystems dividing systems is modeled and applied this method while giving state information of every other subsystems. As a result it can
reduce variable of state in model and prevent state explosion. This paper evaluates eﬀectiveness of modular
veriﬁcation by comparing result of using that method with result of using stepwise method only.

実用的なシステムの検証に多くの適用実績がある [7]．

1 はじめにモデル検査は，検査対象の振舞いモデルをもとに状情報制御システムをはじめとした組込みソフトウェ

態遷移モデルを作成し，状態遷移モデルに対して網アは高信頼性が求められるが，ソフトウェアの大規模羅探索を行うことで期待した性質を満たすか検査す

複雑化により信頼性を確保することが困難になっているものである．そのため，より実践的なモデルに対しる．この問題の解決法の 1 つとして形式手法が挙げ

モデル検査を適用する場合，探索範囲が爆発的に増られ，中でもモデル検査技術は機械的かつ網羅的にシ加する．このように検査対象の状態数が膨大になってステムの品質を保証できることから注目されている．

検査不能になることを状態爆発とよぶ．したがって，

特に，モデル検査器 SPIN は理論ならびに実用の両面

より実践的なモデルに対してモデル検査を適用するから多大な貢献があり，大学・大学院の授業でモデル場合は状態爆発問題に対応することが必要である．

検査の教育に使われるだけでなく，産業界においても

著者らはこれまで情報制御システムを対象に，段階的検査法を用いて状態爆発を防ぐ研究を行ってきた．

Modular veriﬁcation using a stepwise model checking
method in information control systems
Takumi Miyajima,Yoshikazu Ueda, 茨城大学, Ibaraki
University.
Kei Kogai, 茨城工業高等専門学校, Ibaraki National
College of Technology.
Tomoyuki Yamagata,Takayuki Takezawa, 株式会社 日立製作所, Hitachi Co.,Ltd..

段階的検査法は，状態空間を分割しながら，小さな領
域ごとにモデル検査を適用する 1 次処理と分割した
領域間の横断をつなぎあわせて探索を行う 2 次処理から構成されている．これによりモデル検査器による一度に探索する範囲を大幅に削減することができる
が，最小領域に分割しても状態爆発が発生する場合や

ルモデルは仮想環境と制御ルールをもとに制御値を判断，操作指示によって物理環境モデルを操作する．
これを繰り返し実行することで振舞いを表現する．本
論文では，物理環境モデルからの情報の取得から制御
ルールモデルによる操作までの実行をまとめて 1 実
行サイクルとよぶ．また，振舞いモデルは，システムの性質を表す属性を持っている．この属性の組合せを
図1

情報制御システムの構成状態とよび，状態遷移は制御ルールによって状態を変更する．

分割した領域数が膨大になる問題が発生する可能性がある．そこで本論文では，情報制御システムをいく

2. 3 列車運行システムの概要

つかのサブシステムごとに分割し，モジュラ検証する

列車運行システムは列車が安全に移動するために，ことでこれらの問題の解決をはかる．

信号機を用いて列車の移動を制御するシステムである．このシステムの物理環境モデルには以下の設備が2 情報制御システム
2. 1 概要

存在する．
軌道回路

情報制御システムは作業員が手作業で行っていた

線路の最小構成単位を表し，軌道回路を組み合わ設備の制御を自動で行うため，作業員のノウハウをせることで線路が構成される．列車運行システム

ルールとして体系化し，そのルールをもとに自動までは，軌道回路単位で列車の位置を把握する．

たは半自動で設備を制御するシステムのことである．

進路

主に送電や列車運行などの社会インフラの制御システ

複数の軌道回路から構成され，列車の走行ルート

ムとして利用される．情報制御システムの構成を図 1を表す．進路内には基本的に 1 台の列車しか存に示す．情報制御システムは，制御プログラムと実際の物理環境から構成される．制御プログラムは物理環

在しない．
信号機

境のセンサから環境値を取得し，仮想設備に反映させ

必ず 1 つの進路に対応し，点灯状態によって進て制御値を決定し，物理環境に操作指示として制御値路の侵入可否を表す．青色点灯は侵入可能，赤色を出力する．物理環境と制御プログラムは非同期的に点灯は侵入不可を表し，対応進路の列車の在線状連携して動作し，その動作は任意の周期で行われる．
したがって，情報制御システムは任意の周期で仮想設

況によって点灯する色を決定する．
列車

備の更新と制御値の出力を繰り返し実行するシステ

本システムの制御対象を表す．列車は進路に沿っムといえる．

て移動する．進路の終端に到達した場合，次の進路に対応した信号機を確認し，青色点灯している

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

進路へ侵入する．次の進路の信号機が赤色点灯の情報制御システムに対しモデル検査を適用するた

場合は進路変更せずにそのとき在線している進めに，振舞いモデルを作成する必要がある．本研究で路に留まる．

は，図 1 における制御プログラムを制御ルールモデ

上記の物理環境モデルの設備と 2. 2 節の振舞いモデ

ルとしてモデル化し，物理環境を物理環境モデルとし

ルの実行サイクルをふまえて図 2 のような単純な列てモデル化する．これら 2 つのモデルをあわせて振車運行システムの振舞いモデルの例を図 3 に示す．

舞いモデルとする．振舞いモデルの動作は物理環境モ
デルの情報を取得，仮想環境の更新を行い，制御ルー

図2

列車運行システムの例

図4

状態遷移モデルの例

ため検証項目を満たさない．このときモデル検査ツー
ルは検証項目を満たさなかった探索パスを出力する．
この探索パスを反例とよぶ．

3 段階的検査法
3. 1 概要
段階的検査法は以下 2 つのアプローチから構成されている．

1. 状態空間分割
状態空間を分割し，小さな領域ごとにモデル検査を適用することで，一回の検査範囲を小さくし，状態爆発を防ぐ．

2. 属性着目
図3

列車運行システムの振舞いモデル例の一部

検査項目を満たすか探索する際に必要な属性は全体の一部であることに注目し，振舞いモデルの

2. 4 情報制御システムにおけるモデル検査

一部の属性に着目することで，状態爆発を防ぐ．

振舞いモデル作成後，モデル検査ツールに作成し本論文では，検証項目に関係がある属性を着目属た振舞いモデルと検査項目を入力する．本論文では，性とよぶ．列車運行システムにおいては列車の在以下の検査項目について検査を行う．

線位置にあたる．

• 列車が常に同一軌道回路上に複数台存在することがない (列車が衝突しない)

3. 2 実装• すべての列車が進行できず，列車進行のステップ

2 つのアプローチを適用するため，2 段階に分けてを巻き戻すしかない状態にならない (デッドロッ

検証する．段階的検査法によって着目属性に関するグクが発生しない)

ラフ探索問題に帰着させることができる．

モデル検査ツールでは，振舞いモデルをもとに状態遷

3. 2. 1 1 次処理:着目状態間の遷移関係の取得

移モデルを作成し，検査項目をもとに特定の状態へ着目した属性の状態遷移モデルを作成するために，到達可能か探索を行う．作成する状態遷移モデルの例

状態間の遷移関係を取得する必要がある．この状態遷を図 4 に示す．例えば，検査項目が状態 S11 に常に移関係を本論文では部分遷移とよぶ．本論文で対象と到達しないとすると，図 4 の場合，S10 へ遷移するパ

している情報制御システムでは着目属性が物理環境モスが存在しないため，システムは検査項目を満たす．

デルに現れており，明示的に着目属性の組み合わせが検証項目が状態 S9 に常に到達しないとすると，初期分かる．そのため，属性値の組み合わせを網羅的に生状態 S0 から S2 , S5 , S8 を経由して S9 に到達可能な成し，生成した状態集合を 1 つずつ振舞いモデルの入図5

図 4 における 1 次処理の概念図

力として与えて，状態間の部分遷移を取得している．
このとき生成した状態集合を取り出して入力する処理

図6

図 4 における 2 次処理の概念図と遷移関係を記録する役割を状態マネージャとよぶ．
このように明示的に着目属性の組み合わせが分か

3. 3 段階的検査法の正当性らない場合では，着目属性の初期状態から任意の分割

状態空間分割のアプローチは，一度に探索する範範囲を探索し，新たに発見した状態に対して再び分割

囲を限定するだけなので検査結果に影響しないこと

探索を繰り返し実行することで部分遷移の取得が可は明らかである．属性着目のアプローチでは，Cone能である．この場合は状態空間の広がりがなくなるまof Infruence of Reduction 手法 [4] の考え方を用いてで実行する必要がある．

いる．これは，仕様に関係のない変数を除外すること

また，情報制御システムにおいて物理環境の変化によって，状態遷移モデルの大きさを減らす手法であ周期より制御プログラムの実行周期の方が早いので，る．変数の集合である状態 V に対し，仕様と関係の

1 実行サイクルに起こる物理環境の変化は高々一回でない変数を除いた集合である状態 C を定義する．次ある．このことから，状態空間の分割範囲を物理環境に V に対する状態遷移モデルを M，C に対する状態の 1 状態変化とする (着目属性が同時に複数変化する遷移モデルを M̂ と定義し，さらに S を V の全ての部分遷移はない)．

組合せ集合，Ŝ を C の全ての組合せ集合と定義する．
(())
このとき，B ⊆ S × Ŝ : (d1 , ..., dn ) , dˆ1 , ..., dˆk ∈着目属性の状態遷移モデルが図 4 である場合の 1
次処理の概念図を図 5 に示す．

B ⇔ di = dˆi f or all 1 ≤ i ≤ k と定義された関係 B

3. 2. 2 2 次処理:分割領域間の横断の結合が M と M̂ の間で双模倣性関係があることを示すこ

1 次処理によって取得した部分遷移をつなぎ合わせとで正当性を証明している．よって，本論文における状態遷移モデルを生成し，検査項目を満たすか探索を検査に必要としない属性を除外する属性着目アプロー

行う．部分遷移の遷移元が同一の場合や遷移先が同一チを使用することによる検査結果は影響がない．

の場合は部分遷移関係をあわせることで，状態遷移モ
デルに同一状態が複数存在することを防ぐ．初期状態

4 モジュラ検証

から検査項目に違反する状態に到達するか探索によっ

4. 1 システム分割て検査し，発見した場合は反例を出力する．本研究でモジュラに検証する場合，検査対象の振舞いモデル

は，探索アルゴリズムとして深さ優先探索を用いる．

を分割する必要がある．本論文では，検査対象全体を着目属性の状態遷移モデルが図 4 である場合の 2

対象システム，検査対象全体の振舞いモデルを全体

次処理の概念図を図 6 に示す．

モデル，対して分割後の検査対象をそれぞれサブシ
ステム，サブシステムの振舞いモデルをそれぞれ部

図7

システムの全体図

分モデルと定義する．情報制御システムにおいて，分割後のサブシステムも情報制御システムに分類され，各サブシステムが協調して動作することで対象システムを表現できる．システムの全体像を図 7 に示す．

4. 2 サブシステム間の相互関係
本論文では，サブシステム間の関係を相互関係と定図8

モジュラ検証における状態遷移モデルの合成

義し，2 つの相互関係に分類できる．

1. 物理的制約による相互関係
あるサブシステムの物理環境モデルの設備が別のサブシステムの物理環境モデルの設備と同一の場合，物理的制約による相互関係があると定義する．

2. 制御ルールによる相互関係
あるサブシステムにおいて，別のサブシステムの状態によって制御値を決定する制御ルールが存在する場合，制御ルールによる相互関係があると定義する．さらに，この制御ルールをグローバル
ルールと定義し，逆にサブシステム内の状態のみで制御値を決定する制御ルールをローカルルー
ルと定義する．

図9

モジュラ検証時の概念図

4. 3 実装

ステムの状態間を合成することでモデル間の横断をモジュラに検証する場合，他のサブシステムの状

つなぎ合わせる．実際には，相互関係に必要な情報か態を持たないため相互関係を表現できない．そこで，

ら全体システムに状態を拡大したときに，同じ意味

1 次処理時に相互関係に必要な他のサブシステムの状をもつ状態への遷移関係を結合することで合成する．

態を入力として与えることで相互関係を適用する．こサブシステム A の状態 A:S0 とサブシステム B の状

れによって取得できる部分遷移は，着目状態と相互関

態 B:S0 が同義であるときの状態遷移モデルの結合例

係に必要な状態を組み合わせた状態間の遷移関係とを図 8 に示し，モジュラ検証の概念図を図 9 に示す．

なる．2 次処理時には全体モデルの構造から各サブシ

4. 4 モジュラ検証の正当性

4. 4. 3 証明

4. 4. 1 記法定義

分割による影響がないことを示すために以下の式

検査する状態遷移モデル M は，原始命題の集合 APが満たされることを示す．

上で定義される Kripke 構造 M=< S, I, R, L > であMi =< Si , Ii , Ri , Li > f orる．各タプルの定義を以下に示す．

M = M1 ⊗ M2 ⊗ · · · ⊗ Mn

• S は空でない有限状態集合を表す．

(4)

ここで，サブシステムの状態遷移モデルのラベル• I は有限状態集合 S の部分集合 (I ⊆ S) で，初期状態を表す．

関数 Li は (3) より，対象モデルのラベル関数 L を用いても影響がないので，式 (4) は以下の式に変形で• R は遷移関係を表し，R は S と S の直積集合

きる．

の部分集合 (R ⊆ S × S) で表される．ここで，Mi =< Si , Ii , Ri , L > f or

(s1 ∈ S) ∧ (s2 ∈ S) の時，(s1 , s2 ) ∈ R は状態 s1

M = M1 ⊗ M2 ⊗ · · · ⊗ Mn

から状態 s2 へ到達可能であることを表す．

(5)

また，Cone of Infruence of Reduction 手法より，• L はラベル関数で，(s1 ∈ S) かつ状態 s1 におい

検証に関係がない変数を除外しても影響がないことて真である原始命題の集合を返す関数を表す．

が証明されているため，式 (1) が成り立つとき，各サ

4. 4. 2 分割手法定義

ブシステムの状態集合 Si は対象モデルの状態集合 S

対象システムの状態遷移モデルを M，各サブシスを用いても影響がない．状態空間 S を用いることにテムの状態遷移モデルを M1 , M2 , · · · , Mn と定義し，より，初期状態 Ii は初期状態 I を用いる．したがっ

各タプルも同様に定義する．例えば i 番目のサブシスて，式 (5) は以下の式に変形できる．

テムの状態遷移モデル Mi は Mi =< Si , Ii , Ri , Li >Mi =< S, I, Ri , L > f orで表される．サブシステムに分割する場合，対象シス

M = M1 ⊗ M2 ⊗ · · · ⊗ Mn

(6)テムの制御ルールから分割後のサブシステムに必要

式 (6) はある状態からの遷移が M と結合モデル

な制御ルールを選択して部分モデルを作成する．このM1 ⊗ M2 ⊗ · · · ⊗ Mn の双方に含まれれば満たされとき対象システムの制御ルールは必ずいずれかの部る．よって以下の式が満たされればよい．

分モデルに存在し，部分モデルの初期状態は対象シス∃s, s0 f or ((s ∈ S, s0 ∈ S, (s, s0 ) ∈ R)

テムの初期状態と必ず同義の状態を選択する．よって|= ∃i f or (s ∈ S, s0 ∈ S, (s, s0 ) ∈ Ri )) (7)対象システムの状態遷移モデルの状態と遷移関係は∃s, s0 f or (∃i f or (s ∈ S, s0 ∈ S, (s, s0 ) ∈ Ri )|= (s ∈ S, s0 ∈ S, (s, s0 ) ∈ R)) (8)サブシステムの状態遷移モデルのどこかに必ず存在する．したがって以下の式が成り立つ．

(2) より (7)(8) が成立することは明らかである．ゆ(S1 ⊆ S) ∧ (S2 ⊆ S) ∧ · · · ∧ (Sn ⊆ S)
f or S = S1 ∪ S2 ∪ · · · ∪ Sn

えに (1)(2)(3) が成立するモジュラ検証では (4) を満(1)

たし，検証結果に影響を与えることはない．

(R1 ⊆ R) ∧ (R2 ⊆ R) ∧ · · · ∧ (Rn ⊆ R)
f or R = R1 ∪ R2 ∪ · · · ∪ Rn

(2)

(AP1 ⊆ AP ) ∧ · · · ∧ (APn ⊆ AP )f or AP = AP1 ∪ AP2 ∪ · · · ∪ APn

5 適用事例
本章では有効性の評価のために，列車運行システム(3)

ここで記号 ⊗ をモデル結合の意味として定義する．

に対して段階的検査法のみで検証を行った場合とモジュラに検証する場合の結果を比較する．

例えば「M1 ⊗ M2 」は「状態遷移モデル M1 と M2を結合した 1 つの状態遷移モデル」を表す．結合は部

5. 1 対象システムの構成と相互関係

分モデル間で同義の状態をまとめ，遷移関係を結合す

適用する列車運行システムの路線構成を図 10 に示ることで生成される．

す．さらに図 8 をサブシステムに分割した路線構成を
図 11 に示す．この路線構成の場合，通常の信号機の回路位置と在線進路，列車の優先度の組み合わせから
着目状態集合を生成した．モジュラ検証の場合，着目属性集合は部分モデル内の軌道回路位置と在線進路，
列車の優先度に加え，回避ルールに必要になる進路の在線状況の組み合わせから着目状態集合を生成した．

5. 2. 2 着目状態間の遷移関係の取得
着目状態の遷移関係を取得するために，振舞いモ
デルと検査項目に加え，着目状態集合から 1 つずつ
図 10

適用事例の路線構成図

入力として与えて遷移関係を取得する．本論文では状態マネージャを Perl によって実装し，遷移関係を取得するためのモデル検査ツールは SPIN を用いる．

SPIN は一般的に知られているツールであることに加え，モデル記述言語 Promela の c code 記述によって自由に C 言語のコードを追加できる利点がある．これによって着目状態を外部から入力するコードと遷移関係を外部へ出力するコードを振舞いモデルに埋め込むことで 1 次処理を実装する．

5. 2. 3 取得した遷移関係の記録取得した遷移関係を受け取った状態マネージャは，
図 11

適用事例を分割した路線構成図

その情報をデータベースに登録することで管理する．
これは大量に取得できる遷移関係を管理しやすく，遷制御ではデッドロックが発生する．例えば，駅 B の移関係の検索や抽出を効率的に行うことを目的に使ホームに列車が 2 台在線している状態で，駅 A と駅用する．データベースには MySQL を用いて実装をC からそれぞれ駅 B に向けて列車を進行すると，在行った．モジュラ検証の場合，データベースの登録の線している 4 台の列車がすべて進行できない状態とな際に着目状態に付加されている相互関係に必要な状

り，デッドロックとなる．本論文ではこの問題を解決

態と対象モデルの構造から他のサブシステムと同義するために入替信号機 (駅内信号機) の制御ルールにの状態と結合することでモデル間の領域を結合する．

回避ルールを追加する．回避ルールは進行方向先進路

5. 2. 4 部分遷移の結合の在線状況を確認して青色点灯に変えるものである．

2 次処理ではデータベースに蓄えられた情報をもと

以上をふまえ，図 11 のように分割した場合の相互に状態遷移モデルを作成して探索を行う．今回の検査

関係は以下となる．

項目では，性質違反にあたる状態を 1 実行サイクル• 物理的制約：路線間で競合する軌道回路の状態内で発見することができる．そのため状態遷移モデル• 制御ルール：入替信号機に追加した回避ルール

を性質違反状態から生成し，初期状態へ到達するか探索した．性質違反状態から生成することで，すべての5. 2 手法の適用

状態遷移モデルを生成する必要がなくなり，一部の状

5. 2. 1 着目状態の網羅生成

態遷移モデルの探索ですむ．検査項目が活性特性のよ

1 次処理で用いる着目状態を網羅的に生成する．本うに，1 実行サイクル内で発見できない性質の場合は

論文では，デッドロックの発生可能性がある最小台数

初期状態から状態遷移モデルを作成する必要がある．

である 4 台を配置最大数に設定した．このとき，同じ進路に複数台の列車を配置しないように制限し，軌道表1モデルに対する着目状態数

モデル

表4

検査法に対する探索時間の実行結果

着目状態数

対象システム527,337

部分モデル A

59,976

部分モデル B

302,144

部分モデル C59,976

手法

回避

段階的検査

モジュラ検証

13s
○

13s
17s

○

20s

モジュラ検証5. 3 適用実験(4 台制限)

実行時間

13s
○

13s

5. 3. 1 実験結果
適用実験では，正常に動作するモデルと回避ルールを除いた不具合が発生するモデルに対して，段階

表5

検査法に対する総実行時間

手法

回避

実行時間

的検査法のみとモジュラ検証した結果の比較を行う．
対象モデルの着目状態数と各部分モデルの着目状態

段階的検査

1208m(486m48s)○

数を表 1 に示す．部分モデル A と部分モデル C は部
分モデル B を挟んで対称性があるため着目状態数が同じになっている．
次に表 1 を用いて取得した遷移関係数とデッドロッ
ク数，実行時間を表 2 に示す．デッドロック数が対象

モジュラ検証515m46s(148m42s)○

モジュラ検証(4 台制限)1179m52s(460m19s)

496m37s(135m25s)
172m33s(148m38s)○

159m10s(135m18s)※括弧内の時間は DB 登録の時間を除いた実行時間．

モデルより各部分モデルの方が多く出ている原因は部分モデル内でデッドロックが発生しているが他のサため，モデル全体で列車最大数を 4 台に制限したとブシステム側では列車を動かすことができる場合がきとあわせて，検査法に対する各テーブルのレコード含まれていることがあげられる．また，振舞いモデル

数，実行時間を表 3 に示す．

内の列車の最大数を 4 台に設定したため，部分モデ最後に，表 3 を用いて，性質違反状態から初期状

ル内でも 4 台を最大数となっている．そのため部分モ態への到達可能性を探索によって検査する．段階的検デルを結合した場合，全体として 4 台を超える状態

査法のみの場合とモジュラ検証の場合の双方で，回避が発生する可能性がある．よって取得した遷移関係とルールなしの振舞いモデルでは想定したデッドロック

デッドロック数は対象モデルより多く取得している．

の発生を確認し，回避ルールなしの振舞いモデルでさらに表 2 の情報をデータベースに登録する．今は反例の検出は見られなかった．モデルと検査法に対回構築したデータベースは各状態に ID を割り当て，

する実行時間を表 4 に示す．さらに，モデルと検査法

遷移関係を ID 間の関係として扱う．また初期状態とに対する検査の総実行時間を表 5 に示す．表 5 では，エラー状態も各状態の ID で記録する．構築したデー

データベースの登録時間に関して実装方法や使用すタベースは次の 4 テーブルから構成される．

るデータベースに依存することを考え，この時間を除• StList:状態と ID の対応関係の記録するテーブル

いた結果もあわせて示している．

• Init:初期状態を記録するテーブル

5. 3. 2 実験考察

• Err:エラー状態を記録するテーブル

図 10 における検査で 4 台制限の実験結果と比較し• TrList:遷移関係を登録するテーブル

たとき，扱うレコード数に大きな差は現れなかった．

モジュラ検証の場合では，ここでモデル間の横断を考

この原因は相互関係に用いる状態が多く，遷移関係の慮して状態結合を行う．表 2 での状態増加にともな削減効果が得られにくかったことがあげられる．モ

い，遷移関係のレコードが大幅に増加している．そのジュラ検証する場合，サブシステム間の結合度が低い

表2

モデルと着目状態に対する 1 次処理の実験結果

モデル

回避

対象モデル

○

部分モデル A
部分モデル B
部分モデル C

遷移関係数

デッドロック数

実行時間

1,747,980240

486m35s

1,741,260240

460m6s116,128484

26m21s114,256772

26m32s542,848

3,328

95m45s529,216

5,584

82m3s

116,128484

26m19s114,256772

26m30s○○○※回避項目：○は回避ルールあり，正常モデルであることを示す．

表3

手法
段階的検査

モジュラ検証回避○○

モジュラ検証(4 台制限)○検査法に対する DB 登録に関する実験結果

StListInit

Err

TrList

実行時間

557,157

1

30,0601,747,980

721m12s

557,157

1

30,0601,741,260719m33s607,0283

186,036

5,005,328

367m4s607,0283

186,036

4,886,868

361m12s

110,865

3

22,844

999,82024m1s

110,865

3

22,844994,192

23m52sほど相互関係に用いる状態が少なくなり，必要になるは Java Path Finder を対象に，いくつかの実行パス

遷移関係の削減効果が大きい．逆に結合度が高くなを選択し，選択した実行パス間を探索範囲に定め，検るほど効果が低くなり，すべての状態が相互関係に必証を行っていくものである．この研究では，垂直方向要な場合ではモジュラ検証は不可能である (効果がなの分割を実現しており，分割に有効な実行パスを選択い)．そのため，適用事例より結合度の低いシステム

することが難しい問題としてあげられている．本論文に対して適用した場合は，さらなる削減が望める．

では，状態遷移間の分割を実現しているため，分割範モデル検査ツールを使用する着目状態間の遷移関囲の設定は，探索深さの設定によって行われる．

係取得では，モジュラ検証による実行時間の短縮効果[9] は，本論文における段階的検査法の属性着目アが現れている．着目状態数を減らすことができるモ

プローチのもとになった手法である．3. 3 節であげた

ジュラ検証では実行時間が短縮され，さらに状態爆発

検証に関係のない変数を削除する Cone of Influenceへの可能性を減らすことができると考えられる．

Reduction 技術は [4] で紹介されており，一般的に知られた抽象化技法である．他に，Web アプリケーショ

6 関連研究ンに対して検査するプロパティに必要ない状態を無視

これまでの情報制御システムにおけるモデル検査

することで，目的にあわせた状態空間を生成する手法の取り組みがいくつか存在する． [8] は，本論文におが提案されている [6]．

ける段階的検査法の状態空間分割アプローチのもと

また，検査対象の振る舞いモデルに対してモジュになった手法である．他に．探索範囲を限定し，状態ラ検証する研究が数多く存在する． [1] では，Rely-

空間を分割して検証する研究 [3] がある．この研究でGuarantee 技術をはじめとしたモジュラ検証の理論

が紹介されている．Rely-Guarantee 技術は，他のモゴリズムの開発や既存研究の適用によって改善す

ジュールの動作を外部環境として捉え，モジュールとることができると考えられる．また，探索時に活外部環境から検証を行う技術であり，本論文でも同様

性をはじめとした検査特性を解けるようにアルの考え方でモジュラ検証を行っている．この技術を用

ゴリズムを適用する必要がある．

いてモジュラ検証を行う研究も存在し， [2] ではマル

• 更なる有効性の評価

チスレッドのソフトウェアを検証する際に，スレッド

今回の適用事例は，段階的検査法のみでも検査でごとに検証する手法を提案している．各スレッドごときたため，段階的検査法のみでは検証が難しい規に検証を行い，他スレッドの動作を仮想環境として

模の情報制御システムに対してモジュラ検証を適モデル化し検証する． [5] ではプログラムを断片化し，用することで，状態爆発対策の有効性を評価して一度に 1 つの断片化したプログラムと残りのプログいく必要がある．また，結合度が低いモデルに対ラムの仮想環境とともに検証する手法を提案していして適用して，削減効果の確認も行っていく．

る．ここでは，状態の抽象化や対称性による簡約に関しても議論されている．これらモジュラ検証の多くでは，外部環境をモジュールの検査を繰り返すことで生謝辞 本研究は JSPS 科研費 25330075 の助成を受けたものである．

成し，状態空間の広がりがなくなるまで検査する．本
論文では，情報制御システムでの着目属性が既知であ

参 考 文 献る特徴を生かし，外部環境を網羅的に生成することで[ 1 ] Carlo Alberto Furia:A Compositional World - asurvey of recent works on compositionality in formal
methods,Technical Report 2005.22,Dipartimento di
Elettronica e Informazione, Politecnico di Milano,
2005.
[ 2 ] Cormac Flanagan,Shaz Qadeer:Thread-Modular
Model Checking,Model Checking Software Lecture
Notes in Computer Science Volume 2648, 2013, pp.
213-224.
[ 3 ] Diego Funes,Junaid Haroon Siddiqui,Sarfraz
Khurshid:Ranged Model Checking,ACM SIGSOFT
Software Engineering Notes archive Volume 37 Issue 6, 2012, pp.1-5.
[ 4 ] E.M. Clarke, O. Grumberg and D. Peled: Model
Checking, The MIT Press, 1999.
[ 5 ] Kedar S.Namjoshi:Model Checking in Bits andPieces,Electronic Proceedings in Theoretical Computer Science (EPTCS) 129, 2013, pp. 404-416.
[ 6 ] May Haydar,Sergiy Boroday,Alexandre Petreko,Houari Sahraoui:Properties and Scopes in
Web Model Checking,ASE ’05 Proceedings of the20th IEEE/ACM international Conference on Automated software engineering, 2005, pp. 400-404.
[ 7 ] Mordechai Ben-Ari 著, 中島 震 監訳: SPIN モデ
ル検査入門, オーム社, 2010.
[ 8 ] 小山 恭平ら:情報制御システムのモデル検査における状態空間分割による探索手法の提案，ソフトウェア工学の基礎 XIX, 近代科学社, Vol.38, 2012, pp. 39-44．
[ 9 ] 小山 恭平ら:情報制御システムに対する SPIN を用いた段階的モデル検査手法, 日本ソフトウェア科学会創設 30 周年記念大会予稿集, 2013, ippan3-5.

同じ検査を行わなくてよいという特徴がある．

7 まとめと今後の課題
本論文では，検査対象の情報制御システムをいくつかのサブシステムに分割し，それぞれのサブシステ
ムごとに振舞いモデルを作成，段階的検査法を適用することで，モジュラ検査する手法を提案した，本手法の有効性を評価するために，列車運行システムに対して段階的検査法のみで検査した場合とモジュラ検査した場合の遷移関係数と実行時間の比較を行い，一定の短縮効果について示した．本手法の削減効果
は，分割モデル間の結合度が低いほど有効である．今後の課題として次のような課題が挙げられる．

• 2 次処理時の探索アルゴリズムの改善
今回使用した探索アルゴリズムは単純な深さ優
先探索アルゴリズムであるが，これは探索が循環する場合に探索が終わらない問題が発生する可能性があったり，同一状態に何度も探索する可能性があったりと改善する必要がある．着目状態に関するグラフ探索問題を解くために適したアル