(57)【要約】【課題】計算量を削減しつつ的確に非同期反復計算を行う分散システムの形式的検証を行うことができるシステム検証支援装置を提供する。【解決手段】本発明の一実施形態に係るシステム検証支援装置は、複数のノードとこの複数のノード間を接続するリンクとにより構成されたシステムを検証するため、複数のノードの各ノードの初期状態集合、各ノードの遷移関係および複数のノードの到達状態集合にもとづいて、各ノードのそれぞれについて到達状態集合の像計算を行う形式的検証部２２と、像計算により求められた到達状態集合を出力する出力部２３と、を備える。【選択図】  図４
2015018498.tif 000002
【特許請求の範囲】
【請求項１】
複数のノードとこの複数のノード間を接続するリンクとにより構成されたシステムを検証するため、前記複数のノードの各ノードの初期状態集合、前記各ノードの遷移関係および前記複数のノードの到達状態集合にもとづいて、前記各ノードのそれぞれについて到達状態集合の像計算を行う形式的検証部と、
前記像計算により求められた到達状態集合を出力する出力部と、
を備えたシステム検証支援装置。
【請求項２】
前記形式的検証部は、
前記複数のノードの全てについて前記像計算の前後の到達状態集合が一致するまで前記各ノードについての前記像計算を繰り返し、
前記出力部は、
前記複数のノードの全てについて前記像計算の前後の到達状態集合が一致すると、この一致した前記複数のノードの全てについての到達状態集合を出力する、
請求項１記載のシステム検証支援装置。
【請求項３】
前記各ノードの状態変数の定義の情報および前記各ノードでの計算内容を表す関数の情報を含む入力情報を取得する入力情報取得部、
をさらに備え、
前記形式的検証部は、
前記入力情報に応じて前記各ノードの初期状態集合、前記各ノードの遷移関係および前記各ノードの到達状態集合のそれぞれの初期値を設定し、これらの初期値を用いて前記像計算を行う、
請求項１または２に記載のシステム検証支援装置。
【請求項４】
前記入力情報取得部は、
到達状態集合として定常状態集合を前記像計算により求めるよう指示する指示情報を前記入力情報としてさらに取得し、
前記形式的検証部は、
前記入力情報に応じて前記各ノードの遷移関係および前記各ノードの到達状態集合のそれぞれの初期値を設定するとともに、前記各ノードの初期状態集合の初期値として空集合を設定し、これらの初期値を用いて前記像計算を行うことにより前記定常状態集合を求める、
請求項３記載のシステム検証支援装置。
【請求項５】
前記入力情報取得部は、
到達状態集合として到達可能状態集合を前記像計算により求めるよう指示する指示情報を前記入力情報としてさらに取得し、
前記形式的検証部は、
前記入力情報に応じて前記各ノードの初期状態集合および前記各ノードの遷移関係のそれぞれの初期値を設定するとともに、前記各ノードの到達状態集合の初期値として空集合を設定し、これらの初期値を用いて前記像計算を行うことにより前記到達可能状態集合を求める、
請求項３記載のシステム検証支援装置。
【請求項６】
前記出力部により出力された前記複数のノードの全てについての到達状態集合を表示する表示部、
をさらに備えた請求項１ないし５のいずれか１項に記載のシステム検証支援装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、システム検証支援装置に関する。
【背景技術】
【０００２】
所定の仕様に従って設計されたハードウエアやソフトウエアにより構成されるシステムを開発する際には、システムが適切に動作しうるか否かを検証することが重要である。この種のシステムの検証は、一般に、システムの到達可能性解析を行うことにより行われる。システムの到達可能性解析は、システムやシステムのモデルに対して様々な到達可能性アルゴリズム（像計算アプローチ）を適用することにより行われる。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００８−１２３５１７号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
非同期反復計算を行う分散システムなどの複雑なシステムに対してテストやシミュレーションにより検証を行う場合、各ノード（プロセス）の動作タイミングの違いにより計算結果が変化しうるため、テストケースの数が膨大となってしまう。このため、網羅的なテストを行うことは困難である。また、実際のシステムに対して各ノードの動作タイミングを制御することは難しい。また、たとえテストによって問題が見つかっても、現象の再現が難しいため、原因を調べることは難しい。
【０００５】
また、たとえば非同期反復計算を行う分散システムの形式的検証を行う場合、並行性が原因となり、いわゆる状態爆発を起こしてしまうことが多く、検証が非常に困難である。一方、状態爆発を避けるべく、たとえば非同期反復計算における遅延時間を所定の幅以内に収まるものと仮定するなどしてシステムが取りうる状態を制限すると、得られる検証結果の的確性が損なわれてしまう。
【課題を解決するための手段】
【０００６】
本発明の一実施形態に係るシステム検証支援装置は、上述した課題を解決するために、複数のノードとこの複数のノード間を接続するリンクとにより構成されたシステムを検証するため、複数のノードの各ノードの初期状態集合、各ノードの遷移関係および複数のノードの到達状態集合にもとづいて、各ノードのそれぞれについて到達状態集合の像計算を行う形式的検証部と、像計算により求められた到達状態集合を出力する出力部と、を備えるものである。
【図面の簡単な説明】
【０００７】
【図１】本発明の一実施形態に係るシステム検証支援装置の一構成例を示すブロック図。
【図２】検証対象となるシステムと形式的検証ツールとの関係の一例を示す説明図。
【図３】本実施形態に係るシステム検証支援装置による検証対象となるシステムの一例を示す説明図。
【図４】主制御部のＣＰＵによる機能実現部の構成例を示す概略的なブロック図。
【図５】非同期反復計算における通信遅延の様子を説明するための図。
【図６】（ａ）は定常状態集合の計算について説明するための図、（ｂ）は到達可能状態集合の計算について説明するための図。
【図７】従来の到達可能性解析に用いられる従来の形式的検証部の一例を示すブロック図。
【図８】本実施形態の到達可能性解析に用いられる本実施形態に係る形式的検証部２２の一例を示すブロック図。
【図９】図１に示すシステム検証支援装置の制御部のＣＰＵにより、状態爆発を回避するよう計算量を削減しつつ的確に非同期反復計算を行う分散システムの形式的検証を行う処理を実行する際の手順を示すフローチャート。
【図１０】図９のステップＳ２で実行される定常状態集合の計算における初期値の設定処理の一例を示すサブルーチンフローチャート。
【図１１】図９のステップＳ２で実行される到達可能状態集合の計算における初期値の設定処理の一例を示すサブルーチンフローチャート。
【図１２】具体例に用いる分散システムの一例を示す説明図。
【図１３】定常状態集合計算の第１動作例において図９のステップＳ３−Ｓ５が実行されるごとに順次算出される到達状態集合Ｘ１（ｋ）−Ｘ４（ｋ）を示す説明図。
【図１４】定常状態集合計算の第２動作例において図９のステップＳ３の９回目の実行結果を示す説明図。
【図１５】図１２に示す検証対象のシステムのＮ２とＮ３の間のリンクが切れたネットワーク構成を示す説明図。
【図１６】到達可能状態集合計算の動作例において図９のステップＳ３−Ｓ５が実行されるごとに順次算出される到達状態集合Ｘ１（ｋ）−Ｘ４（ｋ）を示す説明図。
【発明を実施するための形態】
【０００８】
本発明に係るシステム検証支援装置の実施の形態について、添付図面を参照して説明する。
【０００９】
（１）概略構成
（１−１）全体構成
図１は、本発明の一実施形態に係るシステム検証支援装置１０の一構成例を示すブロック図である。
【００１０】
システム検証支援装置１０は、入力部１１、表示部１２、ネットワーク接続部１３、記憶部１４および制御部１５を有する。システム検証支援装置１０は、たとえばパーソナルコンピュータやワークステーションなどにより構成することができる。
【００１１】
図２は、検証対象となるシステムと形式的検証ツールとの関係の一例を示す説明図である。また、図３は、本実施形態に係るシステム検証支援装置１０による検証対象となるシステムの一例を示す説明図である。図３には、検証対象システムが４つのノードＮ１−Ｎ４（図３の丸参照）および各ノード間を接続するリンク（図３の直線参照）により構成される分散システムである場合の例について示した。
【００１２】
たとえば図２に示すように、システムの開発過程において、システムの仕様、システムのモデル、システムのプログラムが生成される。本実施形態に係るシステム検証支援装置１０の検証対象は、分散システムの開発過程における分散システムのモデル（設計結果）であってもよいし、実装された分散システムのプログラムであってもよい。検証ツールのスクリプトとは、システムのモデルの内容を形式的検証ツールに入力可能な形式で表現したデータである。本実施形態に係るシステム検証支援装置１０は、形式的検証ツールの内部で実行される到達可能性解析処理を行うために用いられる。
【００１３】
本実施形態に係るシステム検証支援装置１０は、分散システムを検証対象とする。ここで、分散システムとは、複数の情報処理装置の間で通信を行いながら計算処理を進める携帯の情報処理システムをいうものとする。また、以下の説明において、分散システムにおける個々の情報処理装置をノードというものとする。ノードはプロセスと呼称されることもある。また、各ノード間の通信経路をリンクといい、システムを構成する要素であるノードおよびリンクは適宜コンポーネントというものとする。
【００１４】
また、システム検証支援装置１０は通信遅延をあつかうため、分散、並列、並行の用語のうち「分散」システムの用語を用いるものとするが、システム検証支援装置１０は並列計算における非同期処理に適用することも可能であるし、単一の情報処理装置の内部における並行処理に適用することも可能である。
【００１５】
また、モデルとは、システムの動作を表現するために用いられる一定の形式を備えたデータをいい、本実施形態におけるモデルは特に、全状態の集合（そのシステムが取りうる状態の全てを列挙した集合）のデータと、遷移関係を表現するデータと、初期状態の集合のデータが含まれるものとする。また、本実施形態におけるモデルは、初期状態の集合または全状態の集合の初期値のいずれかが与えられない場合についても含む。また。分散システムのモデルにはフェアネス制約が伴うことがある。
【００１６】
一般に、モデルの形式としてはＦＳＭ（Finite State Machine）、ＬＴＳ（Labeled Transition System）、クリプキ構造（Kripke Stracture）などが知られており、本実施形態に係るモデルとしてはどの形式を用いることも可能である。
【００１７】
図１に示す入力部１１は、少なくともポインティングデバイスを含み、たとえばマウス、トラックボール、キーボード、タッチパネル、テンキーなどの一般的な入力装置により構成され、ユーザの操作に対応した操作入力信号を制御部１５に出力する。
【００１８】
表示部１２は、たとえば液晶ディスプレイやＯＬＥＤ（Organic Light Emitting Diode）ディスプレイなどの一般的な表示出力装置により構成され、制御部１５の制御に従って到達状態集合の情報を示す画像などの各種画像を表示する。
【００１９】
ネットワーク接続部１３は、ネットワークの形態に応じた種々の情報通信用プロトコルを実装する。ネットワーク接続部１３は、この各種プロトコルに従ってシステム検証支援装置１０と他の電気機器とを接続する。ここでネットワークとは、電気通信技術を利用した情報通信網全般を意味し、無線／有線ＬＡＮやインターネット網のほか、電話通信回線網、光ファイバ通信ネットワーク、ケーブル通信ネットワークおよび衛星通信ネットワークなどを含む。
【００２０】
記憶部１４は、初期状態集合記憶部１６ｉ、部分遷移関係記憶部１７ｉおよび到達状態集合記憶部１８ｉ（ただし、ｉ＝１、２、・・・、ｎ、ｎは検証対象システムのノードの総数）をそれぞれ検証対象システムのノードの総数ｎと同数ずつ備え、磁気的もしくは光学的記録媒体または半導体メモリなどのＣＰＵにより読み取り可能な記録媒体を含んだ構成を有する。これら記憶媒体内のデータの一部または全部は電子ネットワークを介してダウンロードされるように構成してもよい。
【００２１】
初期状態集合記憶部１６ｉは、ノードＮｉごとに設けられ、各ノードＮｉの初期状態の集合Ｕｉを記憶する。
【００２２】
部分遷移関係記憶部１７ｉは、ノードＮｉごとに設けられ、各ノードＮｉの遷移関係Ｔｉを記憶する。
【００２３】
到達状態集合記憶部１８ｉは、ノードＮｉごとに設けられ、各ノードＮｉの到達状態集合Ｘｉ（ｋ）を記憶する。ただし、Ｘｉ（ｋ）は制御部１５により実行されるｋ回目の像計算の結果により求められる到達状態集合を表す。
【００２４】
ここで、遷移関係について簡単に説明する。ｎ個の集合Ａ１、Ａ２・・・、Ａｎについて、その直積Ａ１×Ａ２×・・・×Ａｎの部分集合をＡ１、Ａ２・・・、Ａｎの間のｎ項関係（n-ary relation）という。特にｎ＝２の場合を二項関係（binary relation）といい、ｎ＝３の場合は三項関係（ternary relation）という。
【００２５】
遷移関係とは、状態遷移を表す関係をいう。本実施形態では、状態の集合をＳとし、状態ｒ∈Ｓから状態ｓ∈Ｓに遷移可能であることの必要十分条件が（ｒ，ｓ）∈Ｔであるとき、Ｔ⊆Ｓ×Ｓを遷移関係という。なお、これは遷移関係が二項関係の場合の定義であるが、モデルの種類によっては三項関係として定義されることもある。本実施形態に係るシステム検証支援装置１０は三項関係など二項関係以外であっても適用可能である。以下の説明では二項関係の場合の例について示す。
（１−２）制御部１５の構成
【００２６】
制御部１５は、ＣＰＵ、ＲＡＭおよびＲＯＭをはじめとする記憶媒体などにより構成され、この記憶媒体に記憶されたプログラムに従ってシステム検証支援装置１０の動作を制御する。
【００２７】
制御部１５のＣＰＵは、ＲＯＭをはじめとする記憶媒体に記憶されたシステム検証支援プログラムおよびこのプログラムの実行のために必要なデータをＲＡＭへロードし、このプログラムに従って、状態爆発を回避するよう計算量を削減しつつ的確に非同期反復計算を行う分散システムの形式的検証を行う処理を実行する。
【００２８】
制御部１５のＲＡＭは、ＣＰＵが実行するプログラムおよびデータを一時的に格納するワークエリアを提供する。制御部１５のＲＯＭをはじめとする記憶媒体は、システム検証支援装置１０の起動プログラム、システム検証支援プログラムや、これらのプログラムを実行するために必要な各種データを記憶する。
【００２９】
なお、ＲＯＭをはじめとする記憶媒体は、磁気的もしくは光学的記録媒体または半導体メモリなどの、ＣＰＵにより読み取り可能な記録媒体を含んだ構成を有し、これら記憶媒体内のプログラムおよびデータの一部または全部は電子ネットワークを介してダウンロードされるように構成してもよい。
【００３０】
図４は、主制御部のＣＰＵによる機能実現部の構成例を示す概略的なブロック図である。なお、この機能実現部は、ＣＰＵを用いることなく回路などのハードウエアロジックによって構成してもよい。
【００３１】
図４に示すように、主制御部のＣＰＵは、システム検証支援プログラムによって、少なくとも入力情報取得部２１、形式的検証部２２および出力部２３として機能する。この各部２１−２３は、ＲＡＭの所要のワークエリアをデータの一時的な格納場所として利用する。
【００３２】
入力情報取得部２１は、ユーザにより入力部１１を介して、またはネットワーク接続部１３を介して他の情報処理装置から、各ノードＮｉの状態変数の定義の情報および各ノードＮｉでの計算内容を表す関数ｆｉの情報を含む入力情報を取得する。入力情報には、到達状態集合として定常状態集合または到達可能状態集合のいずれを形式的検証部２２による像計算により求めるべきかの指示情報が含まれてもよい。
【００３３】
形式的検証部２２は、複数のノードと複数のノード間を接続するリンクとにより構成された分散システムを検証するため、各ノードＮｉの初期状態集合Ｕｉ、各ノードＮｉの遷移関係Ｔｉおよび複数のノードの到達状態集合Ｘ１−Ｘｎにもとづいて、各ノードＮｉのそれぞれについて到達状態集合Ｘｉ（ｋ）の像計算を行うことによりＸｉ（ｋ＋１）を求める。形式的検証部２２は、全てのノードＮ１−Ｎｎについて像計算の前後の到達状態集合Ｘｉが一致するまで各ノードＮｉについての像計算を繰り返す。
【００３４】
形式的検証部２２は、具体的には、初期値設定部３１、部分像計算部３２ｉおよび比較部３３ｉを有する。
【００３５】
初期値設定部３１は、入力情報取得部２１により取得された入力情報に応じて各ノードＮｉの初期状態集合Ｕｉ、各ノードの遷移関係Ｔｉおよび各ノードの到達状態集合Ｘｉの初期値を設定し、それぞれ初期状態集合記憶部１６ｉ、部分遷移関係記憶部１７ｉおよび到達状態集合記憶部１８ｉに記憶させる。
【００３６】
部分像計算部３２ｉは、ノードＮｉごとに設けられ、各ノードＮｉの初期状態集合Ｕｉ、各ノードＮｉの遷移関係Ｔｉおよび複数のノードの到達状態集合Ｘ１−Ｘｎにもとづいて、各ノードＮｉのそれぞれについて到達状態集合Ｘｉ（ｋ）の像計算を行うことによりＸｉ（ｋ＋１）を求める。
【００３７】
比較部３３ｉは、ノードＮｉごとに設けられ、部分像計算部３２ｉにより算出された到達状態集合Ｘｉ（ｋ＋１）と到達状態集合記憶部１８ｉに記憶された到達状態集合Ｘｉ（ｋ）とを比較して一致するか否かを判定する。そして、比較部３３ｉは、全ての比較部３３１−３３ｎで一致すると判定されると、この一致した到達状態集合Ｘｉ（ｋ）を出力部２３に与える。一方、ひとつでも一致しないと、比較部３３ｉは、部分像計算部３２ｉにより算出された到達状態集合Ｘｉ（ｋ＋１）を到達状態集合記憶部１８ｉに記憶させる。この記憶された到達状態集合は、次回の像計算において利用される。
【００３８】
出力部２３は、複数のノードＮｉの全てについて像計算の前後の到達状態集合が一致すると、この一致した複数のノードＮｉの全てについての到達状態集合Ｘｉを出力し、たとえば表示部１２に表示させる。
【００３９】
（２）非同期反復計算
システムの検証担当者が形式的検証ツールを用いる際には、一般に、ツールに入力するためのスクリプトに各ノードや各リンクのモデルを個別に記述し、必要に応じてフェアネス制約も記述しておく。形式的検証ツールはこのスクリプトを入力して、コンポーネントのモデルから分散システム全体のモデルを合成する。
【００４０】
合成されたシステムの全状態の集合は、実行の形態（同期的または非同期的）や、システムの形態（集中、分散、並列など）の違いにかかわらず、各コンポーネントの全状態の集合の直積となることが多い。
【００４１】
このため、非同期反復計算を行う分散システムの到達可能性解析は、全状態の集合の数（状態数）が飛躍的に多くなり状態爆発が起きやすく、実施が困難であった。
【００４２】
ここで、非同期反復計算について簡単に説明する。非同期反復計算（asynchronous iteration）は同期的反復計算（synchronous iteration）の変形であるため、まず同期的反復計算について説明する。
【００４３】
ｎ次元のベクトルｘ（ｋ）（ただしｋ＝０、１、・・・）に対する同期的反復計算では、ベクトルの初期値をｘ（０）からｘ（１）、ｘ（２）、・・・、の順に次の式（１）
に従って計算を進める。
ｘ（ｋ＋１）＝ｆ（ｘ（ｋ））                                        （１）
【００４４】
ただし、ｆは計算処理の内容を表す関数である。非同期反復計算とは異なり、ベクトルに含まれる全ての要素をまとめて更新する。この式をベクトルの要素ごとに書き下すと、ｘのｉ番目の要素をｘｉとして次の式（２）のように書ける。
ｘｉ（ｋ＋１）＝ｆｉ（ｘ1（ｋ）、・・・、ｘｎ（ｋ））               （２）
【００４５】
同期的反復計算は、集中システムでも分散システムでも実行可能であるが、分散システムでは通信によるオーバーヘッドが伴う。
【００４６】
非同期反復計算は、同期的反復計算の変形であり、分散処理の種類のひとつである。同期的反復計算とは異なり、ベクトルの各要素が別々のノードで計算され、そのタイミングや周期もバラバラであり、同期（ノード間の待ち合わせ）は行わない。
【００４７】
また、あるノードから他のノードのデータを参照する際に、通信遅延のためにどの時点の値が得られるかわからないという条件を伴うこともある。通信遅延の量は不定（任意）であり、通信のたびに毎回異なってもよい。また、送信されたデータが必ずしも受信側のノードまで届かなくてもよい。以下の説明では、非同期反復計算にはこれらの仮定が伴っているものとする。
【００４８】
図５は、非同期反復計算における通信遅延の様子を説明するための図である。図５において横軸は時間を表す。また、黒丸は各ノードにおける状態遷移の時点を表す。また、矢印はノード間の通信を表す。
【００４９】
あるノードＮｉで状態を更新する際には、他のノードの過去の状態が参照される。しかし、図５に示すように、他のノードの過去の状態がどの時点の状態であるかは不定である。
非同期反復計算は、次の式（３）のように書ける。
【００５０】
【数１】
2015018498.tif 000003
【００５１】
ただし、α（ｋ）はｋ回目の計算で更新される要素の集合を表し、α（ｋ）⊆｛１、・・・、ｎ｝であり、βｊ（ｋ）は通信遅延の影響を表す。
【００５２】
通常は、αやβｊの具体的な値が指定されることはない。これらは状態遷移のタイミングや通信遅延がバラバラであることを表現するに過ぎないためである。なお、同期的反復計算で収束する（すなわちlimk→∞ｘｋが存在する場合）でも、非同期反復計算では収束しないことがある。
【００５３】
本実施形態に係るシステム検証支援装置１０は、分散システムが初期化されずに稼働開始する場合も扱うため、初期値ｘ（０）が任意の場合も考慮する事ができるようになっている。
【００５４】
本実施形態では、次の３つの条件Ｃ１―Ｃ３を仮定する。なお、Ｃ２とＣ３は、非同期反復計算に固有のフェアネス制約に相当する。
【００５５】
第１の条件Ｃ１は、任意のｋ∈｛１，２，・・・｝に対して０≦βｊ（ｋ）＜ｋという条件である。この条件は、通信で得られる値は過去の値であるという意味の条件である。
【００５６】
第２の条件Ｃ２は、任意のｉ∈｛１，・・・，ｎ｝に対してｉ∈α（ｋ）となるｋは無限にあるという条件である。この条件は、ノードの停止や故障はないという意味の条件であって、待っていればどの要素も必ず更新されることを意味する。
【００５７】
第３の条件Ｃ３は、任意のｌ∈｛０，１，・・・｝と任意のｉ∈｛１，・・・，ｎ｝に対して、βｉ（ｋ）＝ｌとなるｋの集合は有限であるという条件である。この条件は、過去のデータが永遠にノード間のリンク（通信路）に残ることはない、すなわちｘｉ（ｌ）を無限回参照することはないという意味の条件である。
【００５８】
（３）到達可能性解析
本実施形態において、到達可能性解析とは、像計算により何らかの到達状態集合を計算することをいうものとする。到達状態集合には、到達可能状態集合および定常状態集合が含まれるものとする。
【００５９】
到達可能性解析では、状態爆発（状態空間爆発ともいう）という問題が起きやすい。状態爆発とは、計算すべき状態数が爆発的に増えてしまい、メモリ不足で到達可能性解析のためのプログラムが実行できなくなることをいう。
【００６０】
また、像計算とは、遷移関係と状態の集合が与えられた時に、その集合に属する状態から遷移先となりうる状態の集合を求める計算をいい、具体的には、以下に示す式（４）や式（５）の計算をいう。
【００６１】
（３−１）定常状態集合
図６（ａ）は、定常状態集合の計算について説明するための図であり、（ｂ）は、到達可能状態集合の計算について説明するための図である。
【００６２】
図６（ａ）に示すように、定常状態集合は、像計算により、全状態の集合から条件を満たさない状態を削除されて求められる集合である。この集合は、検証対象が同じ状態に無限回繰り返して到達する可能性がある場合に、その状態を列挙した集合である。
【００６３】
正確には、次のように定義される。すなわち、定常状態集合Ｘとは、「ある状態ｓがＸに属することの必要十分条件は、Ｘに属する状態ｒからｓへの遷移が可能である」という性質を持つ集合である。これは、数式によれば次の式（４）のように表される。
Ｘ＝｛ｓ｜∃ｒ．［ｒ∈Ｘ∧（ｒ，ｓ）∈Ｔ］｝                        （４）
【００６４】
この方程式の解Ｘは一意ではないかもしれないが、解が存在するならば他の解を全て含む解Ｘｍａｘが存在する（任意の解Ｘ’に対してＸ’⊆Ｘｍａｘが成り立つＸｍａｘが存在する）。これは、不動点計算における最大不動点に相当する。以下の説明では、このＸｍａｘを定常状態集合というものとする。
【００６５】
（３−２）到達可能状態集合
一方、図６（ｂ）に示すように、到達可能状態集合は、像計算により、初期状態の集合から出発して、この集合から到達可能な状態を加えていくことにより得られる集合である。この集合は、検証対象が到達しうる可能性のある状態を列挙した集合である。すなわち、与えられた初期状態の集合Ｕに属する状態から０回以上の状態遷移により到達する可能性のある状態を列挙した集合を、（Ｕからの）到達可能状態集合という。
【００６６】
正確には、次のように定義される。すなわち、到達可能状態集合とは、「ある状態ｓがＸに属することの必要十分条件は、ｓがＵに属するか、またはＸに属するある状態ｒからｓへの状態遷移が可能である」という性質を持つ集合である。これは、数式によれば次の式（５）のように表される。
Ｘ＝Ｕ∪｛ｓ｜∃ｒ．［ｒ∈Ｘ∧（ｒ，ｓ）∈Ｔ］｝                    （５）
【００６７】
この方程式の解Ｘは一意ではないかもしれないが、解が存在するならば全ての解に共通に含まれる解Ｘｍｉｎが存在する（任意の解Ｘ’に対してＸｍｉｎ⊆Ｘ’が成り立つＸｍｉｎが存在する）。これは、不動点計算における最小不動点に相当する。以下の説明では、このＸｍｉｎを到達可能状態集合というものとする。
【００６８】
（３−３）従来の到達可能性解析
続いて、従来の到達可能性解析の問題点について説明する。
【００６９】
図７は、従来の到達可能性解析に用いられる従来の形式的検証部１２２の一例を示すブロック図である。
【００７０】
従来の形式的検証部１２２は、初期状態集合記憶部１１６、遷移関係記憶部１１７、到達状態集合記憶部１１８、像計算部１３２および比較部１３３を、各１つ備える。これは、本実施形態に係る初期状態集合記憶部１６ｉ、部分遷移関係記憶部１７ｉ、到達状態集合記憶部１８ｉ、部分像計算部３２ｉおよび比較部３３ｉがノードごとに設けられてノードの数ｎと同数設けられるのとは大きく異なる。
【００７１】
従来の初期状態集合記憶部１１６は、状態の集合を記憶し、その内容をＵとして出力する。従来の遷移関係記憶部１１７は、遷移関係を記憶し、その内容をＴとして出力する。従来の到達状態集合記憶部１１８は、状態の集合Ｘ（ｋ＋１）を入力し、それを記憶する。また、記憶している集合をＸ（ｋ）として出力する。
【００７２】
従来の像計算部１３２は、Ｔ、Ｕ、Ｘ（ｋ）を入力とし、次の式（６）で示す計算によりＸ（ｋ＋１）を出力する。
Ｘ（ｋ＋１）＝Ｕ∪｛ｓ｜∃ｒ．［ｒ∈Ｘ（ｋ）∧（ｒ，ｓ）∈Ｔ］｝    （６）
【００７３】
従来の比較部１３３は、Ｘ（ｋ＋１）とＸ（ｋ）を入力とし、両者が等しいか否かを判定する。
【００７４】
なお、従来の像計算部１３２は、フェアネス制約を扱うための複雑な計算には対応できない。すなわち、従来の形式的検証部１２２では、フェアネス制約を扱うことができない。
【００７５】
従来の分散システムに対する到達可能性解析では、検証担当者が個々のノードやリンクのモデルとフェアネス制約を指定することが必要である。このため、到達可能性解析の実行前の準備に多くの工数が必要となってしまうという問題がある。従来の形式的検証部１２２は、検証担当者から与えられたノードやリンクのモデルを合成してシステム全体のモデルを作成する必要がある。このため、システム全体の状態数が大きくなり、到達可能性解析において状態爆発を起こしやすくなってしまう。
【００７６】
特に、非同期反復計算を行う分散システムが検証対象である場合、通信遅延の量が不定（任意）である。このため、過去に送信されたデータを全てリンクのモデルの内部に保持する必要がある。したがって、十分な大きさのバッファを用意する必要があり、そのバッファが状態爆発の原因となってしまう。しかし、通信遅延が所定の範囲に収まるものと仮定して状態数を減らそうと試みると、得られる結果の的確性は大きく損なわれてしまう。
【００７７】
（４）本実施形態に係る到達可能性解析
（４−１）原理
たしかに、非同期反復計算を行う分散システムの到達可能性解析（以下、非同期分散計算という）では、通信の遅延時間が任意である。このため、従来、リンクのモデルは伝搬中の可能性があるデータを全てバッファに保存していた。
【００７８】
しかし、伝搬中のデータとは、そのリンクに接続しているノードの過去の状態を示すデータに他ならない。そして、到達可能性解析においては、過去に到達した状態は、到達状態集合記憶部１１８に記憶されている。したがって、この非同期反復計算の性質を考えれば、到達状態集合記憶部１１８を参照すれば、リンクのモデルを用いる必要がなくなると考えられる。
【００７９】
非同期分散計算では、定常状態集合や到達可能状態集合が、複数の集合の直積となるという性質がある。直積の要素は、個々のノードに対応している。これは、計算結果にノード間の相関関係を含まないことを意味する。換言すれば、相関関係を消去しなければ正しい計算結果が得られない。つまり、遅延時間を考慮しようとすると、状態数が膨大となり計算が大変になってしまうが、遅延時間が不定（任意）であることにより相関関係が消滅するという現象を利用すれば、逆に計算を大幅に簡略化しつつ結果の的確性を保つことができる。
【００８０】
そこで、本実施形態に係る形式的検証部２２は、計算結果をノードごとに分割し、ノードごとに到達状態集合を記憶する到達状態集合記憶部１８ｉを備える。計算結果をノードごとに分割することで、結果として相関関係を消去することにもなる。到達状態集合記憶部１８ｉをノードごとに設ければ、像計算もノードごとに個別に実施することができる。そこで、本実施形態に係る形式的検証部２２は、ノードごとに個別に像計算を実施するための部分像計算部３２ｉを備える。
【００８１】
（４−２）本実施形態に係る形式的検証部２２の構成
図８は、本実施形態の到達可能性解析に用いられる本実施形態に係る形式的検証部２２の一例を示すブロック図である。
【００８２】
図８に示すように、本実施形態に係るシステム検証支援装置１０は、初期状態集合記憶部１６ｉ、部分遷移関係記憶部１７ｉ、到達状態集合記憶部１８ｉ、部分像計算部３２ｉおよび比較部３３ｉがノードごとに設けられてノードの数ｎと同数設けられる。
【００８３】
到達状態集合記憶部１８ｉがノードごとに個別に設けられることにより、ノード間の相関関係が消去される。なお、初期状態集合記憶部１６ｉ、部分遷移関係記憶部１７ｉ、部分像計算部３２ｉおよび比較部３３ｉは必要に応じてまとめてもよいが、分割することにより一度に使用されるメモリ量を削減することができ、計算を高速化することができる。
【００８４】
ノードＮｉに対応するｉ番目の初期状態集合記憶部１６ｉは、状態の集合を記憶し、その内容をＵｉとして出力する。
【００８５】
ノードＮｉに対応するｉ番目の部分遷移関係記憶部１７ｉは、部分遷移関係を記憶し、その内容をＴｉとして出力する。
【００８６】
ノードＮｉに対応するｉ番目の到達状態集合記憶部１８ｉは、状態の集合Ｘｉ（ｋ＋１）を入力し、それを記憶する。また、記憶している集合をＸｉ（ｋ）として出力する。
【００８７】
ノードＮｉに対応するｉ番目の部分像計算部３２ｉは、Ｔｉ、Ｕｉ、Ｘｉ（ｋ）を入力とし、次の式（７）で示す計算によりＸｉ（ｋ＋１）を出力する。
Xi(k＋１)＝Ui∪{si｜∃(r1,・・・,rn）.
[r1∈X1(k)∧・・・∧rn∈Xn(k)∧(r1,・・・,rn,si)∈Ti]}    （７）
【００８８】
ノードＮｉに対応するｉ番目の比較部３３ｉは、Ｘｉ（ｋ＋１）とＸｉ（ｋ）を入力とし、両者が等しいか否かを判定する。そして、比較部３３ｉは、全ての比較部３３１−３３ｎで一致すると判定されると、この一致した到達状態集合Ｘｉ（ｋ）を出力部２３に与える。一方、ひとつでも一致しないと、比較部３３ｉは、部分像計算部３２ｉにより算出された到達状態集合Ｘｉ（ｋ＋１）を到達状態集合記憶部１８ｉに記憶させる。
【００８９】
ここで、部分遷移関係とは、非同期反復計算を行う分散システムにおける、特定のノードに関する遷移関係をいう。ｉ番目のノードＮｉにおける計算内容を表す関数をｆｉとすると、これは非同期反復計算の定義で示した式（３）に等しい。この式（３）で表される関数ｆｉを用いて次の式（８）で定義される（ｎ＋１）項関係が、ｉ番目のノードに関する部分遷移関係である。
Ｔｉ＝｛（ｒ１，…，ｒｎ，ｓｉ）｜ｓｉ＝ｆｉ（ｒ１，…，ｒｎ）｝   （８）
【００９０】
（５）動作
次に、本実施形態に係るシステム検証支援装置の動作の一例について説明する。
【００９１】
（５−１）全体フロー
図９は、図１に示すシステム検証支援装置１０の制御部１５のＣＰＵにより、状態爆発を回避するよう計算量を削減しつつ的確に非同期反復計算を行う分散システムの形式的検証を行う処理を実行する際の手順を示すフローチャートである。図９において、Ｓに数字を付した符号は、フローチャートの各ステップを示す。
【００９２】
まず、ステップＳ１において、入力情報取得部２１は、入力部１１を介して、またはネットワーク接続部１３を介して他の情報処理装置から、各ノードＮｉの状態変数の定義の情報および各ノードＮｉでの計算内容を表す関数ｆｉの情報を含む入力情報を取得する。この各ノードＮｉの状態変数の定義の情報および各ノードＮｉでの計算内容を表す関数ｆｉの情報は、たとえば検証担当者により、形式的検証部２２に入力するためのスクリプトに記述されて入力情報取得部２１に与えられる。また、以下の説明では、到達状態集合として定常状態集合または到達可能状態集合のいずれを形式的検証部２２による像計算により求めるべきかの指示情報が入力情報に含まれる場合の例について示す。
【００９３】
次に、ステップＳ２において、初期値設定部３１は、入力情報取得部２１により取得された入力情報に応じて、各ノードＮｉの初期状態集合Ｕｉ、各ノードの遷移関係Ｔｉおよび各ノードの到達状態集合Ｘｉの初期値を設定し、それぞれ初期状態集合記憶部１６ｉ、部分遷移関係記憶部１７ｉおよび到達状態集合記憶部１８ｉに記憶させる。
【００９４】
次に、ステップＳ３において、ｉ＝１、・・・、ｎについて、ｉ番目の部分像計算部３２ｉは、各ノードＮｉの初期状態集合Ｕｉ、各ノードＮｉの遷移関係Ｔｉおよび複数のノードの到達状態集合Ｘ１（ｋ）、・・・、Ｘｎ（ｋ）を入力し、各ノードＮｉのそれぞれについて到達状態集合Ｘｉ（ｋ）の像計算を行うことによりＸｉ（ｋ＋１）を求める。
【００９５】
次に、ステップＳ４において、ｉ＝１、・・・、ｎについて、ｉ番目の比較部３３ｉは、部分像計算部３２ｉにより算出された到達状態集合Ｘｉ（ｋ＋１）と到達状態集合記憶部１８ｉに記憶された到達状態集合Ｘｉ（ｋ）とを比較して一致するか否かを判定する。ひとつでも一致しないと、比較部３３ｉは、部分像計算部３２ｉにより算出された到達状態集合Ｘｉ（ｋ＋１）を到達状態集合記憶部１８ｉに記憶させ（ステップＳ５）、再びステップＳ３に戻る。一方、全ての比較部３３１−３３ｎで一致すると判定されると、この一致した到達状態集合Ｘｉ（ｋ）を出力部２３に与え、ステップＳ６に進む。
【００９６】
そして、ステップＳ６において、出力部２３は、この一致した複数のノードＮｉの全てについての到達状態集合Ｘｉを出力し、たとえば表示部１２に表示させる。なお、出力部２３は、到達状態集合Ｘｉのうち、たとえば初期設定されたあるいはユーザにより入力部１１を介して指定された所定のノードに対応する１または複数の到達状態集合（たとえばＸ３のみなど）を出力してもよい。
【００９７】
以上の手順により、態爆発を回避するよう計算量を削減しつつ的確に非同期反復計算を行う分散システムの形式的検証を行うことができる。
【００９８】
なお、図９に示す手順において、ステップＳ３で全ての部分像計算部３２１−３２ｎを動作させるとともに、ステップＳ５で全ての到達状態集合記憶部１８１−１８ｎの内容を更新していることに注意する。この部分像計算処理と到達状態集合の更新処理とが別々のステップに分かれていることにより、非同期反復計算に固有のフェアネス制約（上記の条件Ｃ２およびＣ３）が図９の手順に反映されていると言え、非同期反復計算を十分な時間続けた場合にシステム全体としてどのような状態に収束するかを計算することができる。
【００９９】
なお、到達状態集合記憶部１８ｉがステップＳ３において求められた到達状態集合Ｘｉ（ｋ）の全てを記憶している場合には、出力部２３は、ステップＳ３において求められた到達状態集合Ｘｉ（ｋ）のすべてを出力し表示部１２に表示させてもよい。
【０１００】
ここで、図９の手順にフェアネス制約が反映されている原理を簡単に説明する。ノードＮｉが通信によって受け取る他ノードの状態が全てＸ．（０）に属しているならば、ＮｉはＸｉ（１）に属する状態に遷移する。どのノードも停止することはないという仮定（条件Ｃ２）により、どのノードにおいても最低１回は状態遷移が行われた、という時点がいずれは訪れる。この時点をｐ１とする。ｐ１以降、システムの状態はＸ（１）に属することになる。
【０１０１】
一方、ある時点の計算結果を無限回使うことはないという仮定（条件Ｃ３）により、ｐ１以前の計算結果を使わなくなる時点がいずれは訪れる。この時点をｐ２とする。ｐ２以降にノードＮｉが通信により受け取る他ノードの状態は、Ｘ．（１）に属する。
【０１０２】
したがって、ノードＮｉの遷移先はＸｉ（２）に属する。いずれは全ノードで遷移が起きるので、その後は全てのノードの状態がＸ．（２）に属することになる。以上の繰り返しにより、全てのノードの状態がシステム全体としてＸ．（２）、Ｘ．（３）、Ｘ．（４）、・・・、と変化していくことがわかる。このように、Ｘｉ（ｋ）の計算方法には、「いずれはこうなる」という、フェアネス制約の影響で生じるシステムの挙動の傾向が反映されるようになっているのである。
【０１０３】
（５−２）定常状態集合の計算における初期値の設定処理
図１０は、図９のステップＳ２で実行される定常状態集合の計算における初期値の設定処理の一例を示すサブルーチンフローチャートである。
【０１０４】
この手順は、到達状態集合として定常状態集合を像計算により求めるよう指示された場合に実行される。この指示は、たとえば図９のステップＳ１において入力情報として与えられる。
【０１０５】
ステップＳ２１１において、初期値設定部３１は、初期状態記憶部１６１−１６ｎの初期値として空集合を記憶させる。
【０１０６】
また、ステップＳ２１２において、初期値設定部３１は、入力情報に応じて式（８）を用いて各ノードの部分遷移関係を生成し、部分遷移関係記憶部１７ｉに記憶させる。
【０１０７】
また、ステップＳ２１３において、初期値設定部３１は、入力情報に応じて全状態の集合を各ノードの到達状態集合の初期値として設定し、到達状態集合記憶部１８ｉに記憶させ、図９のステップＳ３に進む。
【０１０８】
図９のステップＳ２において図１０に示す手順が実行された場合、Ｕｉは空集合となる。このため、図９のステップＳ３において用いられる式（７）により得られる状態集合は定常状態集合である（式（４）参照）。したがって、図９のステップＳ２において図１０に示す手順が実行された場合、図９のステップＳ４でＹＥＳと判定された時に到達状態集合記憶部１８ｉに記憶されている集合は、各ノードの定常状態集合である。これらの各ノードの定常状態集合の直積が、システム全体の定常状態集合である。
【０１０９】
なお、ステップＳ２１１―Ｓ２１３の順序は記載された順序とは異なる順序で実行されてもよい。
【０１１０】
（５−３）到達可能状態集合の計算における初期値の設定処理
図１１は、図９のステップＳ２で実行される到達可能状態集合の計算における初期値の設定処理の一例を示すサブルーチンフローチャートである。
【０１１１】
この手順は、到達状態集合として到達可能状態集合を像計算により求めるよう指示された場合に実行される。この指示は、たとえば図９のステップＳ１において入力情報として与えられる。
【０１１２】
ステップＳ２２１において、初期値設定部３１は、入力情報に応じて各ノードの初期状態集合を対応する初期状態集合記憶部１６ｉに記憶させる。
【０１１３】
また、ステップＳ２２２において、初期値設定部３１は、入力情報に応じて式（８）を用いて各ノードの部分遷移関係を生成し、部分遷移関係記憶部１７ｉに記憶させる。
【０１１４】
また、ステップＳ２２３において、初期値設定部３１は、到達状態集合記憶部１８１−１８ｎの初期値として空集合を記憶させ、図９のステップＳ３に進む。
【０１１５】
図９のステップＳ２において図１１に示す手順が実行された場合、Ｕｉは空集合ではなく所定の初期状態集合であるため、図９のステップＳ３において用いられる式（７）により得られる状態集合は到達可能状態集合である（式（５）参照）。したがって、図９のステップＳ２において図１１に示す手順が実行された場合、図９のステップＳ４でＹＥＳと判定された時に到達状態集合記憶部１８ｉに記憶されている集合は、各ノードの到達可能状態集合である。これらの各ノードの到達可能状態集合の直積が、システム全体の到達可能状態集合である。
【０１１６】
なお、ステップＳ２２１―Ｓ２２３の順序は記載された順序とは異なる順序で実行されてもよい。
【０１１７】
（６）具体例
続いて、具体例を用いてシステム検証支援装置１０の動作についてさらに説明する。
【０１１８】
図１２は、具体例に用いる分散システムの一例を示す説明図である。
【０１１９】
システム検証支援装置１０によって、図１２に示すＮ１−Ｎ４の４つのノードからなる分散システムを検証する場合を考える。図１２において、ｃｉ,ｊは隣接するＮｉとＮｊとの間の距離を示す。この分散システムは、各ノードＮｉで、基準となるＮ１から各ノードＮｉへの最短経路の長さｄｉを計算することを目的として開発されているものとする。たとえばｄ４、つまりＮ１からＮ４までの距離は、Ｎ１→Ｎ２→Ｎ３→Ｎ４の経路が最短であることから４となる。
【０１２０】
本実施形態に係るシステム検証支援装置１０は、分散システムが設計した目的が本当に達成されるようになっているかどうかを検証するために用いられる。
【０１２１】
以下の動作例の説明では、次の５つの仮定を前提とする。各ノードＮｉは自身のノード番号ｉを知っていること（仮定１）。ｄｉは、Ｎｉがその内部に保持する変数（Ｎｉの状態変数）であること（仮定２）。Ｎｉが隣接ノードＮｊの保持するｄｊの値を必要とする時は、通信によってそれを受け取るが、通信遅延の量は不定であること（仮定３）。隣接するＮｉとＮｊの間の距離ｃｉ,ｊは定数であり、ｃｉ,ｊ＝ｃｊ,ｉが成り立つこと、またその値はＮｉとＮｊの両方があらかじめ知っていること（仮定４）。そして、各ノードの状態変数であるｄｉの初期値は特に指定しない場合は不定とすること、すなわち初期値が任意であること（仮定５）の５つである。
【０１２２】
この種の各ノードＮｉでＮ１から各ノードＮｉへの最短経路の長さｄｉを計算することを目的とする分散システムは、最短距離を定常状態例は、たとえば携帯型通信端末をノードとする場合、通信時にルーティングの経路を決めるときに距離の近いところ（コストの低いところ）を通す場合などに対応する。上記仮定の通り、各ノードは自分の隣にどのノードが存在するかは知っているが、システム全体像は知らない。
【０１２３】
分散システムが目的の通り正しく設計および実装されていれば、分散システムが実行されれば全体像を知ることができる（分散システム自身が自分を認識するということもできる）。システム検証支援装置１０は、本当に実行時にその目指す全体像になることを確認するために用いられる。
【０１２４】
図１２に示す分散システムにおいて、ノードＮｉとの間にリンクが存在するノードをノードＮｉの隣接ノードというものとする。たとえば、ノードＮ４の隣接ノードはＮ２およびＮ３である。
【０１２５】
ｉ番目のノードＮｉでの計算内容を表す関数ｆｉを、次の式（９）のように定義する。
【０１２６】
【数２】
2015018498.tif 000004
【０１２７】
Ｊｉは、Ｎｉの隣接ノードの番号の集合を表す（たとえば、Ｎ４ではＪ４＝｛２，３｝）。式（９）の右辺は「ｉ＝１ならば計算結果を０とし、ｉ≠１ならばｊをＪｉの範囲で変えながらｄｊ＋ｃｉ,ｊを計算し、計算結果をそれらの最小値とする」ことを意味している。
【０１２８】
各ノードは、自ノードの番号をｉとして、ｆｉ（ｄ１、ｄ２、ｄ３、ｄ４）を計算し結果をｄｉに代入することを繰り返す。繰り返しの周期は、不定である。この計算手順は終了せず、無限回の繰り返しを行う。なお、通信遅延も不定であるから、この計算は非同期反復計算である。また、この計算で用いられるｄｊ（他ノードの状態変数）の値は、ノードＮｊとの通信により取得する。このため、通信遅延の影響によりＮｊが実際に保持する直近の値とは異なる可能性がある。
【０１２９】
（６−１）定常状態集合計算の第１動作例
定常状態集合計算の第１動作例は、システムが正しく設計および実装されている場合における例である。この場合、システム検証支援装置１０は、正しく設計および実装されていることがわかる検証結果を出力することが求められる。
【０１３０】
定常状態集合計算の第１動作例では、検証対象の分散システムが、その設計において、各ノードの状態変数であるｄｉのデータ型として符号なしの４ビット整数型（０以上１５以下の値をとる）を採用しているものとする。
【０１３１】
検証担当者が検証したい分散システムの仕様は、「どのような初期状態から出発しても、検証対象の分散システムは正しい結果に収束する」というものであるとする。そこで、検証担当者は、図９および図１０に示す手順によりシステム検証支援装置１０に定常状態集合を計算させ、その計算結果の出力をもとに仕様が満足されているか否かを判断する。
【０１３２】
まず、検証担当者は、図９のステップＳ１で用いられる入力情報としてのスクリプトに次の２つの情報を記述する。１つはＮ１−Ｎ４の状態変数はそれぞれｄ１−ｄ４であって、いずれも符号なし４ビット整数型であるという情報であり、もう１つは各ノードの計算内容を表す関数ｆｉが式（９）で示される関数であるという情報である。
【０１３３】
たとえば、Ｎ１についてはｉ＝１であるから、式（９）からｆ１はゼロとなる。
f１(d１、d２、d３、ｄ４)＝０                                      （１０）
【０１３４】
一方、Ｎ２の隣接ノードはＮ１、Ｎ３、Ｎ４であるから、ｉ＝２、ｊ∈Ｊ２＝｛１、３，４｝を式（９）に代入して、ｆ２は次の式（１１）のように書ける。
f２(d１、d２、d３、d４)＝min｛d１＋c１,２，d３＋c３,２，d４＋c４,２｝  (11)
【０１３５】
このように、各ノードＮｉでの計算内容を表す関数ｆｉの情報が入力情報としてスクリプトに記述される。
【０１３６】
そして、これらの入力情報が入力されると、たとえば図９のステップＳ２で実行される図１０のステップＳ２１２において、入力情報に応じて初期値設定部３１により各ノードの部分遷移関係が生成されるとともに、ステップＳ２１３において、入力情報に応じて初期値設定部３１により各ノードの全状態の集合が各ノードの到達状態集合の初期値として設定される。
【０１３７】
ここで、ノードＮ２に対応する初期値の設定について、例として簡単に説明しておく。
入力情報には、Ｎ２の状態変数ｄ２が符号なし４ビット整数型と定義されている旨の情報が含まれている。このため、全状態の集合Ｓ２は次のように表せる。
Ｓ２＝｛０，１，・・・，１５｝                                    （１２）
【０１３８】
また、ノードＮ２に関する部分遷移関係Ｔ２は、式（８）により次のように書ける。
Ｔ２＝｛(d１，d２，d３，d４，d２’)｜d２’＝f２（d１，d２，d３，d４）｝ (13)
【０１３９】
たとえば、Ｔ２の元には（３，４，１，５，２）、（５，３，４，１，５）、（１，５，３，４，２）などが含まれる。
【０１４０】
同様に、Ｎ２以外のノードについても同様に入力情報に応じて初期値設定部３１により初期値が設定される。
【０１４１】
図１３は、定常状態集合計算の第１動作例において図９のステップＳ３−Ｓ５が実行されるごとに順次算出される到達状態集合Ｘ１（ｋ）−Ｘ４（ｋ）を示す説明図である。図１３において、繰り返しｋ回目に示される到達状態集合Ｘ１（ｋ）−Ｘ４（ｋ）は、ステップＳ３のｋ回目の実行結果を示す。
【０１４２】
図１３に示すように、ステップＳ３の７回目の実行結果は６回目の実行結果と一致する。すなわち、定常状態集合計算の第１動作例においては、Ｘ１（６）×Ｘ２（６）×Ｘ３（６）×Ｘ４（６）＝｛（０，１，２，４）｝が分散システム全体としての定常状態集合である。このため、ステップＳ４の７回目の実行において全ての比較部３３１−３３ｎで一致すると判定され、この一致した到達状態集合Ｘｉ（６）（または到達状態集合Ｘｉ（７））が出力部２３に与えられる。そして、ステップＳ６において出力部２３により表示部１２に部分到達状態集合Ｘｉ（６）が表示される。また、到達状態集合記憶部１８ｉがステップＳ３において求められた到達状態集合Ｘｉ（ｋ）の全てを記憶している場合には、出力部２３は、ステップＳ３において求められた到達状態集合Ｘｉ（ｋ）のすべてを出力し表示部１２に表示させてもよい（図１３参照）。
【０１４３】
検証担当者は、出力部２３による出力を確認することにより、検証対象の分散システムの定常状態集合が｛（０，１，２，４）｝であることを知ることができる。（ｄ１、ｄ２、ｄ３、ｄ４）＝（０，１，２，４）という値は、Ｎ１から各ノードへの最短経路の長さをそれぞれ正しく表している。
【０１４４】
一般に、システムの状態数が有限で、デッドエンド（次の遷移先になりうる状態が存在しない状態）がなく、かつ停止しない（状態遷移を無限回行う）のであれば、そのシステムはどのような初期状態から出発しても、いずれは定常状態集合に含まれる状態に到達し、その後はその状態集合内で遷移する。
【０１４５】
したがって、検証担当者は、「検証対象のシステムがどのような初期状態から出発しても、必ず（０，１，２，４）という状態に到達し、その後もその状態に留まる」ことが確認できる。そして、この状態は分散システムの設計通りの状態である。したがって、検証担当者は、検証対象の分散システムがその設計において採用した各ノードの状態変数ｄｉのデータ型の符号なし４ビット整数型が正しい実装であると判断することができる。換言すれば、システム検証支援装置１０は、正しく設計および実装された分散システムを検証し、確かに正しい定常状態に帰結するという検証結果を出力することができた。
【０１４６】
（６−２）定常状態集合計算の第２動作例
定常状態集合計算の第２動作例は、システムが誤って設計および実装されている場合における例である。この場合、システム検証支援装置１０は、誤って設計および実装されていることがわかる検証結果を出力することが求められる。
【０１４７】
定常状態集合計算の第２動作例では、検証対象の分散システムが、その設計において、各ノードの状態変数であるｄｉのデータ型として符号付きの４ビット整数型（−８以上７以下の値をとる）を採用しているものとする。
【０１４８】
図１４は、定常状態集合計算の第２動作例において図９のステップＳ３の９回目の実行結果を示す説明図である。
【０１４９】
第１動作例と同様の手順により図９の手順を実行すると、ステップＳ３の１０回目の実行結果は９回目の実行結果と一致する。すなわち、定常状態集合計算の第２動作例においては、図１４に示すＸ１（９）−Ｘ４（９）が検証対象のシステムの定常状態集合である。
【０１５０】
検証担当者は、出力部２３による出力を確認することにより、検証対象の分散システムの定常状態集合に複数の要素が含まれていること、および最短経路の長さとして明らかに誤った値である負の値が含まれていることを知ることができる。
【０１５１】
したがって、検証担当者は、検証対象の分散システムがその設計において採用した各ノードの状態変数ｄｉのデータ型の符号付き４ビット整数型が誤った実装であると判断することができる。換言すれば、システム検証支援装置１０は、誤って設計および実装された分散システムを検証し、確かに誤った定常状態に帰結するという検証結果を出力することができた。
【０１５２】
また、図１４に示す誤った定常状態集合の出力結果を用いることにより、検証担当者は、正常動作しないことの原因を探ることも可能である。
【０１５３】
たとえば、Ｘ２（９）に−８が含まれていることから、検証担当者は次のように原因を推測可能である。すなわち、ｄ４＝４のときにｄ４＋ｃ４,２＝８となる。しかし、この値は符号付き４ビット整数型の範囲（−８以上７以下）に収まらないため、−８と解釈されてしまう。この結果、Ｎ２の状態変数ｄ２＝―８となる。この影響が他のノードにも伝搬することにより、ｄ２ｄ３ｄ４の値が変化を続けてしまい、システムが特定の状態に収束しないという現象が起きる。したがって、到達可能性解析の結果は、この現象が原因である。
【０１５４】
このように原因を推測できると、検証担当者は、たとえばｄｉを符号なし４ビット整数型に変更すべき、あるいは符号付き５ビット整数型に変更すべきなどの解決策に想到する。実際、符号付き５ビット整数型であれば、第１動作例と全く同じ結果を得ることができる。すなわち、符号付き整数型を使う場合でも、ビット長が十分であれば正常に動作することが、システム検証支援装置１０の出力にもとづいて容易に推測することができる。
【０１５５】
（６−３）到達可能状態集合計算の動作例
次に、定常状態集合計算の第１動作例により（ｄ１、ｄ２、ｄ３、ｄ４）＝（０，１，２，４）という定常状態に達した後、図１２に示す検証対象のシステムのＮ２とＮ３の間のリンクが切れた場合について考える。
【０１５６】
図１５は、図１２に示す検証対象のシステムのＮ２とＮ３の間のリンクが切れたネットワーク構成を示す説明図である。
【０１５７】
図１５に示すシステムは、図１５から明らかなようにＮ１から各ノードへの最短経路の長さはそれぞれ（ｄ１、ｄ２、ｄ３、ｄ４）＝（０，１，４，５）である。したがって、本動作例では、（ｄ１、ｄ２、ｄ３、ｄ４）＝（０，１，２，４）という初期状態から出発して、リンク切れ後のシステムが（ｄ１、ｄ２、ｄ３、ｄ４）＝（０，１，４，５）に至る仮定で、どのノードが影響を受けるかを調べることができれば非常に便利である。
【０１５８】
そこで、検証担当者は、各ノードの初期状態集合Ｕｉの初期値を（０，１，２，４）とし、そこで、図９および図１１に示す手順によりシステム検証支援装置１０に到達可能状態集合を計算させ、リンク切れによりどのノードが影響を受けるかを判断する。
【０１５９】
定常状態集合計算の第１、第２動作例と同様に、まず、検証担当者は、図９のステップＳ１で用いられる入力情報としてのスクリプトに各ノードＮｉの状態変数の定義および各ノードの計算内容を表す関数ｆｉを記述する。そして、これらの入力情報が入力されると、たとえば図９のステップＳ２で実行される図１１のステップＳ２２１において、入力情報に応じて初期値設定部３１は、各ノードの初期状態集合が初期状態集合記憶部１６ｉに記憶させるとともに、ステップＳ２２２において、入力情報に応じて初期値設定部３１により各ノードの部分遷移関係が生成される。
【０１６０】
図１６は、到達可能状態集合計算の動作例において図９のステップＳ３−Ｓ５が実行されるごとに順次算出される到達状態集合Ｘ１（ｋ）−Ｘ４（ｋ）を示す説明図である。図１６において、繰り返しｋ回目に示される到達状態集合Ｘ１（ｋ）−Ｘ４（ｋ）は、ステップＳ３のｋ回目の実行結果を示す。
【０１６１】
図１６に示すように、ステップＳ３の４回目の実行結果は３回目の実行結果と一致する。このため、ステップＳ６において出力部２３は、表示部１２に部分到達状態集合Ｘｉ（３）を表示させる。
【０１６２】
検証担当者は、出力部２３による出力を確認することにより、検証対象の分散システムにおいて、ノードＮ１およびＮ２は、Ｎ２とＮ３間のリンク切れの影響を受けないことがわかる。また、Ｘ３（３）およびＸ４（３）にも極端な値は含まれていないことから、検証担当者は、収束に至る過程において、Ｎ３やＮｆでオーバーシュートによる行き過ぎが発生することはないと判断することができる。
【０１６３】
本実施形態に係るシステム検証支援装置１０は、非同期反復計算を実行する分散システムに対する到達可能性解析において、定常状態集合や到達可能状態集合が、複数の集合の直積となるという非同期反復計算の性質を利用し、計算結果をノードごとに分割し、ノードごとに到達状態集合を記憶する到達状態集合記憶部１８ｉを備える。このため、リンクのモデルが不要になるとともに、使用するメモリ量が減少する。したがって、本実施形態に係るシステム検証支援装置１０によれば、状態爆発を回避するよう計算量を削減しつつ的確に非同期反復計算を行う分散システムの形式的検証を行うことができる。
【０１６４】
従来の形式的検証部１２２は、最大で、検証対象の分散システムの全状態の集合を記憶させる必要がある。各ノードの全状態の数をそれぞれｍ１，・・・，ｍｎとすると、全ノードを合成した結果の状態数は、ｍ１，・・・，ｍｎの積となる。また、リンクのモデルも必要であるため、システム全体のモデルの状態数は、さらに多くなる。
【０１６５】
一方、本実施形態に係るシステム検証支援装置１０は、各ノードに対応する到達状態集合記憶部１８ｉに記憶させる状態数は、それぞれ最大でｍ１，・・・，ｍｎである。このため、システム全体のモデルの状態数は、ｍ１，・・・，ｍｎの和となる。
【０１６６】
実用的な意味のある検証対象では、ｍ１，・・・，ｍｎはそれぞれ２以上であることが多い。このため、ｍ１，・・・，ｍｎの和は、ｍ１，・・・，ｍｎの積よりも大幅に小さい。したがって、本実施形態に係るシステム検証支援装置１０は、従来に比べあつかう状態数を大幅に削減することができ、状態爆発を回避することができる。
【０１６７】
また、ノードのモデルを合成してシステム全体のモデルを作成する必要がないため、使用メモリ量をさらに削減することができる。
【０１６８】
また、従来は、検証担当者が形式的検証ツールにフェアネス制約を指定する必要があった。また、従来の形式的検証部１２２だけでは、そもそもフェアネス制約に対応できなかった。一方、本実施形態に係る形式的検証部２２により実行される図９に示す手順には、非同期反復計算に固有のフェアネス制約が反映されている。このため、検証担当者は、フェアネス制約をあえて指定する必要がなく、非常に利便性が高い。また、システムの設計者と検証担当者が同一である場合には、たとえば各ノードの状態変数の定義をいろいろとためしつつ各定義を実装した場合の形式的検証を行うことができる。したがって、本実施形態に係るシステム検証支援装置１０によれば、システム開発に要する時間を大幅に短縮することができる。
【０１６９】
また、本実施形態に係るシステム検証支援装置１０は、関数ｆが不動点をもたない場合も扱うことができる。関数ｆが不動点をもつ場合には、それは定常状態集合に含まれる。一方、ｆが不動点をもたない場合でも、複数の状態を順に訪問して元の状態に戻るような状態遷移のループが存在するなら、定常状態集合は空ではない。
【０１７０】
なお、本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【０１７１】
たとえば、非同期反復計算の定義にはベクトルを用いたが、各ノードがあつかうデータは、実数、整数や複素数などの数値データに限られない。本実施形態に係るシステム検証支援装置１０は、各ノードが他のノードに割り込まれることなく（すなわちアトミックに）記憶装置に書き込み可能なデータの組みを、ベクトルの１つの要素に対応するものと考える。したがって、ベクトルの１つの要素が、分散システムのプログラムにおいては複数の変数に対応することもある。
【０１７２】
また、本実施形態に係るシステム検証支援装置１０は、種々の非同期分散計算の形式的検証に適用することができ、たとえばマルチコアプロセッサがマルチスレッド動作をしている場合にスレッド間通信をするときに、同期プリミティブなしで動かすシステムの検証に用いることができる。
【符号の説明】
【０１７３】
１０  システム検証支援装置
１２  表示部
２１  入力情報取得部
２２  形式的検証部
２３  出力部
【図１】
2015018498.tif 000005
【図２】
2015018498.tif 000006
【図３】
2015018498.tif 000007
【図４】
2015018498.tif 000008
【図５】
2015018498.tif 000009
【図６】
2015018498.tif 000010
【図７】
2015018498.tif 000011
【図８】
2015018498.tif 000012
【図９】
2015018498.tif 000013
【図１０】
2015018498.tif 000014
【図１１】
2015018498.tif 000015
【図１２】
2015018498.tif 000016
【図１３】
2015018498.tif 000017
【図１４】
2015018498.tif 000018
【図１５】
2015018498.tif 000019
【図１６】
2015018498.tif 000020