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

情報制御システムに対する SPIN を用いた
段階的モデル検査手法
小山 恭平

小飼 敬

上田 賀一

山形 知行

武澤 隆之

モデル検査において，モデルの状態は全ての属性の値の組合わせから構成される．そのため，属性が増えると検査範囲は爆発的に大きくなる．そこで本研究では，段階的にモデル検査を行うことで検査範囲を部分化する手法を提案する．提案手法では，まずモデルを用いて状態の部分遷移履歴を抽出する．次にその部分遷移履歴をつなぎ合わせ，状態遷移モデルを作成する．この状態遷移モデルに対して網羅探索することによって，意図した振舞いが起こるか検査する．本手法の有効性を示すため, 列車進路制御システムにおいて従来手法との比較を行った．適用実験から提案手法が従来手法より優れていることを示す.

検査不能に陥る可能性が高い．モデル検査において，

1 はじめに探索範囲が膨大になることでメモリ上に状態を記憶で機能安全の国際規格である IEC6108 の安全性イきなくなり，検査が不可能になることを「状態爆発」

ンテグリティレベル (SIL) において，最高レベルのと呼ぶ [5]．モデル検査を実システムに適用するためSIL4 で形式手法の使用が強く推奨されていることかにはこの状態爆発に対する対策がほぼ必須である．

ら，形式手法を用いたシステムの品質保証に注目が集本研究は情報制御システムへモデル検査を適用すまっている [3]．形式手法とは数学的理論に基づいたることを目的とする．情報制御システムはインフラ系設計，開発及び検証の総称である．形式手法におけるの制御システムとして使用され，不具合が発生すると検証手法のひとつとしてモデル検査が存在する．

人命や社会生活に甚大な影響を及ぼす可能性がある．

モデル検査とは，モデルを用いたシステムの振舞いそのため情報制御システムには高い信頼性や安全性シミュレーションにおいて，モデルの状態を調べるこが求められ，モデル検査による品質検査が必要とされとにより意図した振舞いが起こるかを検査する手法でている．

ある．このとき，状態はモデル内の全属性の値の組合モデル検査を適用可能にするため，状態爆発対策とわせから構成されるため，属性が増えると検査範囲はして段階的にモデル検査を行うことで検査範囲を部爆発的に大きくなる．モデル検査用ツール SPIN で分化する手法を提案する．本手法によって検査対象のは状態をすべて記憶するため，探索範囲が爆発的に大状態を選別することができる．よってモデル検査に必きくなると必要なメモリの量も爆発的に大きくなり，要となるメモリ量を削減できるため，情報制御システムに対してモデル検査が適用可能となる．

Step-by-step model checking method using SPIN forInformation Control System
Kyohei Oyama, Yoshikazu Ueda, 茨 城 大 学, Ibaraki
University.
Kei Kogai, 茨城工業高等専門学校, Ibaraki National
College of Technology.
Tomoyuki Yamagata, Takayuki Takezawa, 株式会社 日立製作所, Hitachi Co.,Ltd.

2 情報制御システム
2. 1 概要
情報制御システムとは，作業員が手動で行っていた操作を自動化するため，操作手順等のノウハウをルールとして体系化し，ルールベースで自動的に設備を操!"#$%&'()
図2
図1

検査モデルの構造図

情報制御システムの概念図作するシステムである．主に列車進路制御や電力送電等のインフラ系の制御に用いられる．
情報制御システムは制御ブログラムと物理環境から構成される．物理環境は複数のセンサや設備から構成され，制御プログラムはセンサからの環境情報を基に設備に操作指示を与える．

2. 2 制御プログラムの動作制御プログラムは次の動作を周期的に実行する．

1. センサーから物理環境の情報を取得する

図3モデルの流れ

図4

状態遷移の例

2. 取得した情報を基にプログラム内部の仮想設備の状態を更新する

3. 仮想設備の状態と制御ルールを基に、実行すべき操作を決める

4. 物理環境の設備へ操作指示を送信する
この動作を図示したものが図 1 である．

2. 3 モデル検査
情報制御システムの構造及び制御プログラムの動作から，検査モデルは図 2 のようになる．検査モデ
ルは制御ルールモデルと物理環境モデルの 2 つから構成される．

全体が動作する．このサイクルを図 3 に示す．
情報制御システムのモデル検査は図 2 の検査モデ
ルを用いて，任意の状態 (初期状態) から特定の状態制御ルールモデルは物理環境モデルから環境情報に到達するかどうかを検査する．例えば検査モデルのを取得し，設備への操作指示の内容を決定する．物理

状態遷移が図 4 の場合，状態遷移を辿って状態 S0 か

環境モデルは操作指示を基に物理環境に存在する設ら状態 Si に到達できるかどうかを調べる．本論文に備の状態を非決定的に変化させる．このため，制御おいて，この手法を従来手法と呼ぶ．

ルールモデルによる制御指示の決定と物理環境モデルによる設備の状態変化が 1 サイクルとなる，このサイクルを繰り返し実行することにより検査モデル

も「設備 A」に関する検査だった場合，物理環境モデルの状態遷移から「設備 A 属性 A」と「設備 A 属性B」の 2 つが変化する状態遷移のみを調べれば良い．
このように検査目的に関係のある属性は検査モデル内の全属性のうち一部のみの可能性がある．そこで，検査モデル内の属性のうち検査目的に関係のある属性が変化する状態遷移を取得し，状態遷移モデルを作成する手法を提案する．
図5

モデルと属性の例

提案手法の流れを次に示す．

1. 検査モデルから検査目的と関係のある属性を抽
2. 4 モデル検査の問題点
図 2 に示した検査モデルを用いて，従来手法でモデル検査を実行しようとした場合，状態爆発が発生して検査不能となる可能性が高い．
検査モデルの状態は複数の属性から構成される．属性は複数の属性値をもっており，状態は理論上その属性値の組合わせ分存在する．そのため属性数が増えると組合わせによって状態数が膨大になり，状態爆発出する

2. 抽出した属性において，属性値の全組合わせを生成する (状態の生成)

3. 検査モデルを用いて，状態間の遷移関係を取得する (部分遷移履歴の取得)

4. 遷移履歴を基に状態遷移モデルを作成する(状態遷移モデルの作成)
5. 状態遷移モデルを網羅探索するが発生する．例えば，図 5 に示す検査モデルでは物理環境モデルの属性が 5 個，制御ルールモデルの属

3. 2 各段階の詳細性が 6 個の計 11 個の属性が存在する．このとき，11

3. 2. 1 状態の生成個の属性がそれぞれ 10 個の属性値を持つとする．そ検査に関係のある属性に対して属性値の全組合わの場合，組合わせから状態数は 1000 億個となる．
このとき必要となるメモリ量は，単純計算するとせを生成し，状態としてデータベースに保存する．

3. 2. 2 部分遷移履歴の取得

4bit/属性 × 11 属性 × 10 状態 より 550TByte とな

生成した状態間の遷移関係の取得には情報制御シる．このため，通常のコンピュータでは明らかにすべステムの検査モデルを使用する．そのため，図 2 とての状態をメモリに記憶できないため，図 5 の検査

図 3 に示した検査モデルに対して 3 つの変更を行う．

11モデルに対してモデル検査を適用すると状態爆発が• 外部から状態を読み込み可能にする発生する．

• サイクルの動作回数を 1 に制限• 状態を外部に出力可能にする

3 段階的モデル検査

1 つ目に関して，Promela では c code という記述を

3. 1 概要

用いて C のコードを検査モデル内に埋め込むことが前章で述べたとおり，検査モデル内の属性が増える可能である．これを用いてファイルから状態を読みと探索範囲は爆発的に大きくなるため，状態爆発が発込み可能にした．状態読み込み用のコードを図 6 に生し検査不能になる可能性が高い．そのため，状態爆示す．

発対策が必要となる．
本手法では検査目的と属性の関係に着目する．例
えば図 5 に示す検査モデルに対して，物理環境モデ2 つ目に関して，状態間の遷移関係を取得するには検査モデルを 1 サイクルだけ動作させれば良いので，1 サイクル動作したら終了するように変更した．

ルに関する検査を行う場合，物理環境モデルの状態3 つ目に関して，入力方法と同様に c code を用い遷移のみが必要となる．また，物理環境モデルの中でて，検証目的と関係のある属性の変化直後に変化後の

1234567

void inputTrainInfo(){char s[256];
FILE ∗fp;
int valueA, valueB ,valueC, index;
if((fp =fopen(”input.dat”,”r”)) == 0){exit(EXIT FAILURE);}

89101112131415161718

trainIndex = 0;
while(fgets(s,256,fp) != 0){sscanf(s,”%d,%d,%d”,&valueA,&valueB,&valueC);
now.equipmentA[trainIndex].attributeA = valueA;
now.equipmentA[trainIndex].attributeB = valueB;
now.equipmentA[trainIndex].attributeC = valueC;
trainIndex++;}fclose(fp);
}

図6

1
2
3
4
567

図8

遷移関係取得の流れ

状態取得用 Promela コード

void outputTrainInfo(){FILE ∗fp;
char s[256];
int i = 0;if((fp = fopen(”output.dat”, ”a”)) == 0){exit(EXIT FAILURE);}

図9

状態遷移モデル生成の例

89101112131415161718for(i = 0; i < TRAIN MAX;i++){fprintf(fp, ”%d,%d,%d\n”,now.equipmentA[i].attributeA,now.equipmentA[i].attributeB,now.equipmentA[i].attributeC);}
fprintf(fp,”−−−−−−−−−−−−−−−−−\n”);
fclose(fp);}る．遷移関係の取得はデータベースに保存した全状態に対して行う．

3. 2. 3 状態遷移モデルの作成
部分遷移履歴に対して，遷移先となる状態を基に遷移同士を繋げることで状態遷移モデルを作成する．
状態遷移モデル作成の例を図 9 に示す．この図が示すように，例えば 0 → 1 の遷移であれば，遷移先の状態 1 はさらに状態 2 と状態 3 に遷移する．よって

図7

状態出力用 Promela コード

0 → 1 と 1 → 2，1 → 3 の遷移を繋げる．これを全ての遷移に対して実行する．

状態を出力するように検査モデルを変更した．外部へ状態を出力するコードを図 7 に示す．

4 適用事例

この検査モデルを用いて，状態間の遷移関係を取提案手法の有効性を示すため，図 11 と図??に示す

得する．まず任意の状態を検査モデルに入力する．次駅における列車進路制御システム (以下，対象システに検査モデルが 1 サイクル分動作するなかで，状態ム) に対してモデル検査を適用する．従来手法での検が変化したらその状態を外部へ出力する．動作終了

査結果と検査コストを比較し，提案手法によって従来後，入力状態と出力状態を部分遷移履歴としてデータ手法と等価な検検査がより低コストでできることをベースに保存する．これを図示したものが図 8 であ示す．なお，以下において図 11 を中規模駅，図??を図 12
図 10進路, 信号機, 軌道回路の例

デッドロックの起こらない中規模駅-./045&'()*+,

図 11!

デッドロックの起こらない中規模駅"#$%!

145 23

小規模駅と呼ぶ．
図 13

列車進路制御システムの概念図

4. 1 対象システムの説明
4. 1. 1 列車進路制御システムの概要

4. 1. 2 列車進路制御プログラムの動作

列車進路制御システムとは列車が安全に駅内を移制御プログムは次の動作を周期的に実行する．

動できるように，信号機を用いて列車の移動を制御するシステムである．そのため，駅における物理環境として次に示す設備が存在する．
軌道回路
線路の対象構成単位である．列車は軌道回路単位で移動する．
進路

1. 列車がどの進路のどの地点にいるのか(走行情報) を取得する
2. 走行情報を基に仮想設備を更新する
3. 進入を許可する進路を判断する
4. 許可進路を保有する信号機には青色点灯指示を，それ以外の信号機には赤色点灯指示を出す

4. 1. 3 物理環境の動作

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

物理環境において次の動作が実行される．

ト．進路内には基本的に高々1 台の列車しか存在• プログラムの指示によって信号の点灯状態が変しない．
信号機

わる• 列車が非決定的に進路内を移動する

列車進路制御プログラムから指示を受けて，自• 列車が非決定的に駅外から進入してくる身の点灯状態を変更する．信号機は必ずひとつ• 進路の終端に到達した列車は，信号機の点灯状の進路に対応する．信号機の点灯状態は進路へ態に従って，現在の進路と物理的に接続しているの進入可否を表しており，青色点灯は進入許可，赤色点灯は進入不可を表す．
列車

進路に非決定的に移動する

4. 1. 4 検証目的
物理環境においてデッドロックが発生するかどうか制御したい対象．列車は信号機の点灯状態に従を検査する．ここで，次の 3 つの条件を満たす状態

い，進路に沿って移動する．列車には通常列車，をデッドロックと定義する

分割列車，結合列車等の種類がある．
これらの設備を具体的に図示したものが図 12 である．
またシステム全体の概念図は図 13 となる．

1. 移動可能な列車が存在しない．
2. 1 の状況において，列車が進入したい進路の中で青色点灯できる信号機が存在しない3. 列車が駅に進入できない
124. 2 前提条件

3

今回の適用実験の前提条件として，次の条件を定義

4する．

• 中規模駅，小規模駅の両方で駅内の最大列車在線数は 4 とする• 列車は通常列車のみを対象とする

56
781012

4. 3 提案手法におけるモデル検査

13

4. 3. 1 列車在線状態の生成

14るため，列車に関する属性のみがあれば良い．検査モ

hidden Array Table[N STATE];

911

検査目的は物理環境におけるデッドロック検知であ#define MAX 最大分岐数#define N STATE 状態数
typedef Array{
int num = 0;
int values[MAX] = −1;};

15c code{char buf[256];
int source = 0int index = 0
int destination = 0;
FILE ∗fin;1617

fin = fopen(”matrix.dat”, ”r”);

18

デルのなかで，列車に関する属性は次の 3 つである． 19
なお列車以外の属性のリストは省略する.

• 走行している進路• 進路内での位置

20
21
2223

• 列車種別24

列車の在線数を 0〜4 台として，これらの属性の組

25

合わせ (列車走行状態) を網羅的に生成しデータベー26

スに登録した．

27
28

if(fin == NULL){ exit(1);}while(fgets(buf, 256, fin) != NULL){if(buf[0] != ’\0’){sscanf(buf, ”%d,%d”,&source, &destination);
Table[source].values[Table[suorce].num] =destination;
Table[suorce].num++;}}
fclose(fin);};4. 3. 2 列車走行状態の遷移履歴の取得
図 2 に示す検査モデルを用いて，列車走行状態間

図 14

状態遷移表の作成部分の遷移関係を取得し部分遷移履歴としてデータベースに保存した．

表1

実験環境

4. 3. 3 列車走行状態遷移モデルの作成

メモリ

8GB 1333MHz DDDR3

今回の事例では，状態遷移モデルの探索を SPIN で

CPU2.3Ghz Intel Core i7行う．そのため，状態遷移モデルを状態遷移表で表現

OS

Mac OS X 10.6.8

した．Promela モデルにおける状態遷移表の作成部分を図 14 に示す．

4. 4 実験結果

ここで，部分遷移履歴はファイル matrix.dat に記

実験を行った環境を表 3 に示す．この環境下におい録されており，そこから一行ずつ読み込んで Table にて，提案手法の検査結果と検査コストを従来手法と比記録していく．

較した．

4. 3. 4 網羅探索

4. 4. 1 検査結果の比較作成した状態遷移表に対して網羅探索を実行する．

小規模駅において反例が出力された．デッドロック

今回のモデル検査ではデッドロックの定義を満たす状態に到達するかどうかを調べる．

として出力された状態を図 15 と図 16 に示す．
提案手法と従来手法でデッドロックとして出力された状態は，両方ともデッドロックの条件を満たしている．そのため，提案手法において従来手法と同じ検査ができたと言える．しかし，2 つの状態を比較する

表2
中規模

従来
提案
従来
提案

小規模
図 15

従来手法における反例

表3
中規模
小規模
図 16

提案手法における反例と進行方向の違う列車が 2 台存在する．従来手法にの探索順によるものだと考えられる．

4. 4. 2 検査コストの比較

中規模
小規模

2台
414182
1404
19494
1289

3台
6201402
6210
99984
2517

4台
×145361247*
236*

列車台数とメモリ使用量 (Mbyte)

従来
提案
従来
提案

1台36.77
6.06
9.19
5.30

表4

列車台数と処理時間 (sec)おいて反例を全て出力した結果，提案手法で出力された反例が含まれていることから，この原因は SPIN

列車台数と状態数

1台
9338
1191459151

従来
提案
従来
提案

1台
0.18
1.79
0.034
1.61

2台
1009.17
7.59
43.79
5.49

2台
7.60
8.86
0.31
3.38

3台
3027.429.11
169.675.49

3台
114.02
76.91
1.55
11.83

4台
×10.0114.34*
5.49*

4台
×614.020.11*
36.78*

中規模駅，小規模駅，それぞれのモデル検査における検査コストとして，メモリ使用量及び処理時間を比手法の方が SPIN の使用するメモリが少ないことが較する．実験結果における前提を次に示す．

分かる．提案手法において，部分遷移取得では SPIN• 提案手法において，処理時間は，状態の生成，部

は対象システムの 1 サイクル分しか動作させないた

分遷移履歴の取得，状態遷移モデルの作成，網羅めメモリ使用量が少ない [4]．また状態遷移モデルの探索の時間を合計したもの網羅探索では，検査目的に関係のある属性のみで状態• 提案手法において，メモリ使用量は部分遷移履を構成することで探索範囲を部分化していることから歴の取得と網羅探索において SPIN が使用したメモリ使用量が少ない．このため，全体として SPIN最大のメモリ量のメモリ使用量が少なくなった．

• 提案手法において，状態遷移モデルの自動作成処理時間に関しては，小規模モデルにおいては従来プログラムを Java で使用しており JavaVM の手法の方が短時間で検査できるという結果になった．

ヒープ領域のサイズは規定値 (1GByte) を使用し提案手法では部分遷移履歴をデータベースに記憶すているることや複数回 SPIN を実行することが必要となる• 従来手法において，中規模駅で最大列車配置数ため，大量のオーバヘッドが存在する．そのため，探が 3 以上の場合は SPIN の状態圧縮オプション

索範囲が狭い場合は従来手法よりも時間が掛かる．し(COLLAPSE オプション) を使用している

かし，中規模モデルにおいては 3 台以降で提案手法• 提案手法において，状態数は状態遷移モデルに対する網羅探索における状態数である• *印の結果は反例を見つけたことにより，途中でモデル検査が終了している
モデル検査の検査コストを表 3 と表 4 に示す．また表 2 には各状況における状態数を示す．ここで．メ
モリ使用量に関しては，どちらの駅に対しても提案の方が短時間で検証できるという結果になった．これは探索範囲の部分化による時間縮小がオーバヘッドとなる処理の時間を上回ったからであると考えられる．
また，中規模モデルで列車の最大配置数を 4 台にした場合，従来手法では 10 時間以上経過しても検査が終了しなかったため検査不能と結論付けた．

以上のことから，SPIN のメモリ使用量に関しては，モデルの規模に関係なく提案手法の方が優れて6 まとめおり，モデル規模が大きくなっても最大 1GByte+数

本論文では，検査モデル内の属性増加による状態爆Mbyte のメモリがあれば検査可能である．またモデ発を防ぐため段階的にモデル検査を実行することで，ルの規模が大きくなるほど，処理時間においても提案検査目的に関係のある属性のみの状態遷移モデルを手法の方が優れた結果を出せるといえる．

構築し，検査する手法を提案した．本手法の有効性を示すため，列車進路制御システムに対して，提案手法

5 関連研究を適用し従来手法と比較した．結果として，従来手法

情報制御システムのモデル検査に関する以前の取より少ないメモリで検証可能であり，従来手法では検り組みとして，状態空間分割による探索手法 [4] があ証できなかった状況 (中規模駅で列車の最大配置数 4る．この手法では，状態空間を複数回に分けて探索す台) においても検証が可能であった．また駅の規模がることで，状態爆発を防いでいる．本論文で提案して大きくなると，提案手法の方が短時間で検証可能といる手法は，この分割探索の手法を部分遷移履歴の取なった．

得において利用している．分割手法では事前に用意し本手法は検査目的に関係のある属性における状態た状態の遷移に問題があるかを検査するため，検査で遷移のみを抽出している．そのため，検査モデルを検きる性質に限りがあった．それに対して，本手法では査目的に関係のある属性のみで再構成した場合と比状態遷移モデルを構築することにより SPIN で検査較すると，オーバヘッドがある分提案手法の方が検査可能な性質のすべてに対応可能である．

コストがかかる．しかし再構成した場合，検査モデルモデル検査における状態爆発対策の研究として，を変更しているので，元の検査モデルとの等価性を調Cormac ら [1] と松原ら [2] の研究がある．Cormac らべる必要がある．それに対して，本手法では検査モデの研究 [1] では遷移の依存関係を動的に発見すること

ルから遷移情報を取得するだけで，検査モデルを変更で，状態遷移モデルの探索パスを減らす手法を提案ししないため等価性を調べる必要がない．ている．この手法では悪い状態に到達しないかどう

実際の情報制御システムには運用上の制約が存在か (安全性) の検査のみを対象としている．しかしモするが，今回は対象外としている．しかし，部分遷移

デル検査の性質ではもうひとつ，良い状態にいずれ到履歴から状態遷移モデルを構成する際に，運用上の制達可能かどうか (活性) の検査が存在しており，これ約を考慮して繋ぐことで対応可能である．そのため，には対応していない．本手法では任意の属性のみで状今後は運用情報を基にした遷移の接続が課題となる．

態遷移モデルを構成するだけであり，その状態遷移モデルに対する探索を規定していない．そのため安全性

参 考 文 献と活性の両方を検査することが可能である．

[ 1 ] Cormac Flanagan，Patrice Godefroid：DynamicPartial-Order Reduction for Model Checking Software，POPL’05，pp.110-121(2005)．
[ 2 ] 松原正裕，桜井康平，成沢文雄，山中久光：ハードウェア異常に対応した組み込み制御ソフトウェア不具合のモデル検査手法，情報処理学会研究報告．EMB，組み込みシステム 2012-EMB-24(11)，pp1-5(2012)[ 3 ] 中島震：ソフトウェア工学の道具としての形式手法，
NII Technical Report(2007)．
[ 4 ] 小山恭平，小飼敬，上田賀一，山形知行，武澤隆之，
中野利彦：情報制御システムのモデル検査における状態空間分割による探索手法の提案，ソフトウェア工学の基
礎 XIX pp.39-44, 近代科学社 (2012).
[ 5 ] 吉岡信和，青木利晃，田原康之 著，萩原昌己 監修：
SPIN による設計モデル検査，近代科学社 (2008)．

松原らの研究 [2] では，モデル内の変数依存関係によるスライシングを用いることで，検査目的に合わせたモデルの詳細化レベルの変更を行っている．そのため，検査目的に合わせた検査手法という点で本研究と共通している．しかし松原らの手法が検査目的に合わせた検査モデルの構築であるのに対して，本手法は検査目的に合わせた状態遷移モデルの構築である．
そのため，本研究とはアプローチの方向性が異なっている．