1　はじめに
社会インフラを支える大規模な制御システムで障害が置きてしまうと，人命や生活に大きな影響を与えるため，システムの品質保証が必要となっている.そこで，形式手法の一種であるモデル検査が注目されている。モデル検査とは，検査対象のシステムの振舞い仕様をモデル化し，モデルの取りうる状態を網羅的に探索することで，期待する性質を満たすか検証する手法である．これにより，従来は人手で行っていた工程を機械的かつ網羅的に行うことができるので,大規模システムであっても品質を保証することが可能である。しかし，実務で利用すると検査対象の規模の大きさから，検査が終了しないという状態爆発問題が起きてしまう[1].さらに，モデル検査による検証結果から実システムの問題箇所を特定することが困難となる問題も存在している.本研究の先行研究では， 1次処理として状態爆発を防ぐために状態空間を複数の部分に分割し，モデル検査を適用している。２次処理として空間を状態空間をまたぐような検証を行い，問題があれば反例を出力する．本研究では，検証結果において出力される反例から問題箇所を特定するために，剖御ルールの並びに着目した反例分析手法を提案する。先行研究ではデータベースとしてリレーショナルデータベースを利用しているが，本研究ではグラフデータベースの利用についても検討する.
2  先行研究
2.1情報制御システム本研究が対象とする情報制御システムは，作業員が手作業で行っていた制御を自動化するために，作業員のノウハウを制御ルールとして体系化し，設備を自動で制御するシステムである。具体的には，制御プログラムと物理環境から構成され、制御プログラムは制御ルール・仮想設備・仮想センサから構成され，物理環境は設備・センサ・制御対象から構成される．制御用プログラムはセンサから制御対象情報を取得し，取得した情報と制御ルールから設備への操作指示を出力する。情報制御システムは，仮想環境の値を更新し，訓御を繰り返すシステムといえる．
2.2 状態爆発問題
モデル検査では，状態を網羅的に探索するため，調べる状態が非常に多くなる可能性がある。状態は属性値の組であるため，属性値の組み合わせ分だけ状態数が存在する。たとえば2個の属性がそれぞれ，10個の属性値を持つ場合，状態は10² = 100状態となるが，属性の数が２倍になると，10 4 = 10000状態となり，状態数が指数関数的に増加する．検査する振舞いによっては，コンピュータのメモリに入りきらないくらいの状態を調べなければならなくなり，モデル検査ツールにより検査できないという問題が生じることがある。この問題を状態爆発問題と呼ぶ。状態爆発問題はモデル検査における解決するべき問題の１つとなっている[1].
2.3 段階的検査手法
段階的検査手法とは，状態爆発問題を防ぐために考案されたモデル検査手法である[3]. 具体的には，伏態空間を分割して小さな領域ごとにモデル検査を適用する。段階的検査手法の処理はl次処理と2次処理に分かれている。 1次処理では振舞いモデルの分割を行う。分割方法としては，制御ルールによって変化する状態に注目し，訓御ルールによる相互関係を少なくするような箇所で分割を行う[2].  ２次処理では,分割された状態空間をまたぐような検証を行う．分割された状態空間を合成して検証を行うのだが，すべての状態に対して合成状態を作成してしまうと状態爆発が起きることが分かっている。そのため，検証内容に応じて必要な部分のみ合成しながら検証を行う.
2.4グラフデータベース
グラフデータベースとは、データの構造が全てグラフ構造で表されるデータベースである。リレーショナルデータベースとは異なり，NoSQLに分類され，ノード・リレーションシップ・プロパティなどの概念が存在する．実用例としては，SNSにおける友達の友達を検索したり，ネットショッピングにおける「この商品を買った人はこんな商品も買っている」のようなことを表示するために使われている。このように, ２つのノードの最短距離などの計算が高速に行えることが特徴となっており，もう１つの特徴として，クエリ言語の可説性が高いことも挙げられる。代表的なグラフデータベースとしてNeo4jがあり，Cypherと呼ばれるクエリ言語を使用してグラフを検索する.
3　反例分析手法
3.1ツールの開発
本研究の先行研究では，反例の原因を単体ルールが原因の場合，ルール不足や寒行優先度が原因の場合，ルールの組み合わせが原因の場合の３つとしている[4].これらの原因を調べるために４つの検索方法を寒装した.
1.ルール単体検索
ルール単体検索では，反例パスと同じルールが正例で適用されているかどうかを検索する。あるルールが反例パス上でのみ適用されている場合は，そのルール単体で反例の原因となっている可能性がある。そのため，本ツールでは反例パス上でのみ適用されているルールが存在するならば,そのルールを出力する.
2.状態分岐検索
状態分岐検索では，反例パス上の状態から正例への状態に遷移させるようなルールが存在するかどうかを検索する。正例への遷移を持たずに反例となる場合はルールが不足している可能性がある。また，反例にならない遷移を持っているにも関わらず反例となってしまう場合は，ルールの実行優先度が原因の可能性がある．そのため，本ツールは反例パスの上の状態からの分岐が存在するならばその状態とルールを出力する.
3.ルール順序検索
ルール順序検索ではパターンマッチングを用いる。まず，反例パスから任意の長さの状態列を抜き出す.その状態列で適用されたルールのリストをR'とする。すべてのパスにおいてパターンマッチングを行い，R'と一致するパターンを持っているパスを検索結果として出力する．反例パスと同じルールが反例パスのみで適用されている場合は，適用ルールの順番に原因がある可能性がある．検索の例として，反例パスから３個取り出した場合R' = R 1 , R 2 , R 3となり，検索するルールリストは(R1, R2, R3),(R1, R2),(R2, R3)
となる.
4.ルール順列検索
ルール順列検索では，ルール順序検索でのルールリストR'内の要素の組み合わせR"をもって，ルール順序検索と同様の検索を行う．つまり，反例パスに適用されているルールを順不同で適用しているパスを検索する。ルール順序検索と同様に，適用ルールの組み合わせに原因がある可能性がある．検索の例として， R' = R 1 , R 2 , R 3の場合の検索するルールリストはR" =(R1, R2, R3),(R1, R3, R2),(R2, R1, R3), (R 2 , R 3 , R 1 ),(R 3 , R 1 , R 2 ),(R 3 , R 2 , R 1 )となる次に使い方を説明する。まず，ルール単体検索を行い，ルール単体で反例の原因になっているかを調べる。次に状態分岐検索を行い，反例パスの構造を把握する。最後にルール順序検索・ルール順列検索を行い，反例パスでのみ適用されているルールの並びを調べる。反例パスでのみ適用されているルールの並びが存在すれば，それらを確かめることで反例の原因を特定する手がかりになると考える.また，実行時間の比較を行うために，利用するデータベースが異なり同じ機能を持つツールを２通り実装した。ただし，リレーショナルデータベースであるMySQLを使用する場合，ルール順序検索・ルール順列検索のようなグラフを走査するような探索の場合は遅くなることが既に分かっている。そのため，文字列化処理を行う。これは，データベースに保存されて
いるすべてのパスを文字列としてメモリに確保し，その文字列を検索することで実行時間を早めるものである.
4適用実験
本研究の対象である制御システムにおいて本ツールを使用し実験を行い、反例の原因を特定できるかどうか確かめる。また，２つのツールの実行時間の比較を行う。今回の実験で使用する反例パスについては,検査項目に違反している遷移にマーキングを行い，初期状態からその遷移をしたパスを別ファイルとして保存し，到達可能性について検査した結果として扱う.実験環境について表1に示す.
4.1適用事例
情報制御システムの一種であるエレベータの制御システムを適用事例とする。このシステムは，呼び出しポタンや階指定ポタンの情報から建物内のエレベータの動きを倒御し，円滑にエレベータを移動させるシステムである．今回実験に適用したエレベータ制御システムは、エレベータと各フロアに取り付けられた呼び出しポタンから構成されており，建物の階数が３階，エレベータが１つ，定員は１人となっている．エレベータ情報を表2, フロア情報を表3, 制御ルール一覧を表4に示す。また，エレベータのステートマシン図を図１に示す.違反する検査項目については，エレベータが定員オーバーのまま移動してしまうようなモデルを作成した．全体として，状態数247,040個，遷移数232,000個となった.
4.2実験結果
4つの検索結果について以下に示す。また，２つのツールはどちらも同じ結果となる.反例パス上のみに適用されているルールは存在しなかった。そのため，ルール単体が反例に影響していないことが考えられる. ●ルール単体検索●状態分岐検索
反例パス上から正例へのパスは存在しなかった.すべての反例パスが分岐せずに初期状態から反例へ遷移していた．そのため，反例から正例に遷移するようなルールが不足している可能性が考えられる.
反例パス上にしか存在しないルールの適用順序を発見した。ルールが(1,6,9,5,8,19,19,17,2,5,8)の聞番で適用されているパスは反例パスのみとなっていた.表３より，具体的な動作を確認する．エレベー夕内の乗員が現在より下の階指定ポタンを押し,下降を開始している。しかし，ルール17によって既に乗っていた乗員の目的階に到達する前に,待機している人がいる階で停止し，尿を開けている。 1人目が降りていない状態で２人目が乗ったまま尿が閉まり，エレベータが下降しようとしていることが分かる。また，上昇中においても同じ現象が反例上で起きていた．反例パスのみに存在する最短のルールリストは(2,5,8),(2,4,7)となった.
ルール順序検索の結果である(2,5,8),(2,4,7)について検索を行った結果，組み合わせを変えた場合については正例と反例のどちらにも存在しなかった以上から，ルールを(2,5,8),(2,4,7)の順番で適用した場合に反例となる可能性が高いことが考えれれる.また反例になる前の遷移にルール7やルール8が適用されている。これらのルールはドアを閉めるルールであるため，ドアを閉める処理をする前に，定員オーバーになっているかを判定する処理を追加することで，反例になることを防ぐことができると考えられる.
4.3実行時間の比較
4.2節の実験をするにあたり，実装した２つのツールの実行時間の比較を行った．また，MySQLを利用する場合においては，3.1節で記述した通り，文字列化処理を行った場合についても比較を行った。今回のモデルについては文字列化処理に約37分かかった.実行時間が極端に長くなるものについては実験を中断した.ルール単体検索・状態分岐検索の実行時間を表5,ルール順序検索の実行時間を表6, ルール順列検索の実行時間を表7, それぞれのグラフを図2, 図3に示す.

4.4考察
反例が存在するモデルに対して実験を行った結果,反例の原因を見つける手助けを行うことができた．反例パスのみに適用されているルールリストを見つけることができれば、反例の原因を特定できると考えられる。実行時間については，文字列化処理を考慮した場合，状態分岐検索以外においてグラフデータベースであるNeo4jを利用した方が速いことが分かった.
リレーショナルデータベースにおいてグラフ構造をたどるには，１つの遷移を調べるごとに遷移後状態を遷移前状態として検索することを繰り返すためクエリが複雑になり，さらにループ判定を行う必要があるため処理が遅くなってしまうことが分かる.一方,グラフデータベースでは１つのクエリで検索を行うことができるため，処理が高速になっていることが分かる．今回実装した機能はグラフ構造を把握する必要があるため，グラフデータベースであるNeo4jが速い結果となった．しかし，状態分岐検索では１つの遷移ごとに検索を行うため，１つの遷移ごとに格納されているリレーショナルデータベースであるMySQLの方が速い結果となった、データベースによる差が大きかったため，実装言語の差については比較を行っていない.
5まとめ
本研究では，制御ルールの適用順序に着目した反例分析ツールを開発し，エレベータ制御システムのモデルに対して実験を行った．また，利用するデータベースの違いについて比較を行った．反例パスにおけるルールの順序に着目することで，反例の原因特定の手助けを行えることを示した．また，グラフ構造のデータを解析する場合はリレーショナルデータベースよりもグラフデータベースの方が優秀であることを示した．今後は，他のモデルに対して実験を行い，検査者に対してさらにわかりやすく結果を出力できるように寒装を行う.本研究を進めるにあたり，ご協力くださった(株)日立製作所インフラシステム社の武澤隆之様，山形知行様，テクノロジーイノベーションセンタの奏野康生様に深く感謝いたします[1] 吉岡信和,青木利晃,田原康之: SPINによる設計モデル検証, 2008. [2]古木隆裕,小飼敬,上田賀一:情報制御システムのモデル検査におけるモデル分割支援法の検討，日本ソフトウェア科学会大会論文集, Vol. 33(2016), pp. 453–460. [3] 小山恭平,小飼敬,上田賀一:情報制御システムに対するSPINを用いた段階的モデル検査手法,日本ソフトウェア科学会大会論文集, Vol. 30(2013), pp. 274–281. [4] 大森祐貴,小飼敬,上田賀一:段階的検査法を用いたモデル検査の反例分析手法,日本ソフトウェア科学会大会論文集, Vol. 32(2015), pp. 6p.