(57)【要約】【課題】コンピュータシステムの安全性検査を高速に行い、かつ有限の時間内で検査を終了させることを可能とする安全性検査装置を提供する。【解決手段】入力部１０は、状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、コンピュータシステムが安全でない状態を示す集合の情報と、繰り返し状態遷移を行った際に無限に到達状態を発生させない状態を表現する局所言語を算出するための拡張情報とを入力して記憶部２０へ記録する。極限計算部３０は、記憶部３０に記憶されているシステム状態遷移規則の情報と拡張情報とに基づいて初期状態から局所言語を算出し、算出した局所言語を用いてコンピュータシステムの状態を表現した第２の有限オートマトンの情報を生成して出力する。安全性判定部４０は、初期状態の集合の情報と安全でない状態を示す集合の情報と、第２の有限オートマトンの情報とに基づいて安全性の判定を行う。【選択図】    図１
2007004236.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータシステムの状態を有限文字集合の文字列で表現する有限オートマトンの情報に基づいて、前記コンピュータシステムの安全性を判定する安全性検査方法であって、
前記コンピュータシステムの状態を示す状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、前記コンピュータシステムが安全でない状態を示す集合の情報と、前記コンピュータシステムの状態遷移の任意の回数の繰り返しを表現するオートマトンを有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力して記憶手段へ記録するステップと、
前記記憶手段から前記システム状態遷移規則の情報と、前記拡張情報とを読み出し、読み出した前記システム状態遷移規則の情報と、前記拡張情報とに基づいて、前記局所言語を算出するステップと、
算出した前記局所言語を用いて前記コンピュータシステムの状態遷移規則の任意の回数の合成を近似的に表す第２の有限オートマトンの情報を生成して出力するステップと、
前記記憶手段から前記初期状態の集合の情報と前記安全でない状態を示す集合の情報とを読み出すステップと、
読み出した前記初期状態の集合の情報と、前記安全でない状態を示す集合の情報と、前記第２の有限オートマトンの情報と、に基づいて安全性の判定を行うステップと、
判定された安全であるか、あるいは安全でないかを示す判定結果を出力するステップと、
を含むことを特徴とする安全性検査方法。
【請求項２】
コンピュータシステムの状態を有限文字集合の文字列で表現する有限オートマトンの情報に基づいて、前記コンピュータシステムの安全性を判定する安全性検査装置であって、
前記コンピュータシステムの状態を示す状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、前記コンピュータシステムが安全でない状態を示す集合の情報と、前記コンピュータシステムの状態遷移の任意の回数の繰り返しを表現するオートマトンを有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力して記憶手段へ記録する入力手段と、
前記記憶手段から前記システム状態遷移規則の情報と、前記拡張情報とを読み出し、読み出した前記システム状態遷移規則の情報と、前記拡張情報とに基づいて、前記局所言語を算出し、算出した前記局所言語を用いて前記コンピュータシステムの状態遷移規則の任意の回数の合成を近似的に表す第２の有限オートマトンの情報を生成して出力する極限計算手段と、
前記記憶手段から前記初期状態の集合の情報と前記安全でない状態を示す集合の情報とを読み出し、読み出した前記初期状態の集合の情報と、前記安全でない状態を示す集合の情報と、前記第２の有限オートマトンの情報と、に基づいて安全性の判定を行う安全性判定手段と、
前記安全性判定手段によって判定された安全であるか、あるいは安全でないかを示す判定結果を出力する出力手段と、
を備えたことを特徴とする安全性検査装置。
【請求項３】
コンピュータシステムの状態を有限文字集合の文字列で表現する有限オートマトンの情報に基づいて、前記コンピュータシステムの安全性を判定する安全性検査装置のコンピュータに、
前記コンピュータシステムの状態を示す状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、前記コンピュータシステムが安全でない状態を示す集合の情報と、前記コンピュータシステムの状態遷移の任意の回数の繰り返しを表現するオートマトンを有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力して記憶手段へ記録するステップと、
前記記憶手段から前記システム状態遷移規則の情報と、前記拡張情報とを読み出し、読み出した前記システム状態遷移規則の情報と、前記拡張情報とに基づいて、前記局所言語を算出するステップと、
算出した前記局所言語を用いて前記コンピュータシステムの状態遷移規則の任意の回数の合成を近似的に表す第２の有限オートマトンの情報を生成して出力するステップと、
前記記憶手段から前記初期状態の集合の情報と前記安全でない状態を示す集合の情報とを読み出すステップと、
読み出した前記初期状態の集合の情報と、前記安全でない状態を示す集合の情報と、前記第２の有限オートマトンの情報と、に基づいて安全性の判定を行うステップと、
判定された安全であるか、あるいは安全でないかを示す判定結果を出力するステップと、
を実行させるためのコンピュータプログラム。
【請求項４】
請求項３に記載のコンピュータプログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータシステムの安全性の検査に用いられる安全性検査方法、安全性検査装置及びコンピュータプログラム並びに記録媒体に関する。
【背景技術】
【０００２】
コンピュータシステムの安全性検査方法についてこれまで様々な研究が行われている。コンピュータシステムの安全性検査とは、一定の状態遷移規則によって動作するコンピュータシステムが、初期状態から動作を開始したときに、状態遷移の繰り返しによって安全でない状態に遷移しないことを確かめることである。コンピュータシステムの安全性検査方法として、例えば、モデル検査という技術が知られている（非特許文献１参照）。
【０００３】
また、特に、コンピュータシステムの状態が有限の文字集合上の文字列を用いて表され、初期状態の集合、安全でない状態の集合および状態遷移規則が全て正則言語を用いて表される場合に用いられるモデル検査技術として、正則モデル検査という技術が知られている（非特許文献２参照）。正則モデル検査の技術では、有限オートマトンを用いて正則言語を表現できることを利用して、初期状態の集合、安全でない状態の集合および状態遷移規則を有限オートマトンを用いて表し、有限オートマトンの演算を繰り返すことにより安全性検査が行われる。
【非特許文献１】E.M. Clarke, O.Grumberg and D.Peled.”Model Checking.” MIT Press, p1-p49, 2000.
【非特許文献２】P.A. Abdulla, B.Johnsson, M.Nilsson, and M.Saksena. “A survey of regular model cheking.” In Proc. 15th Int. Conf. on Concurrency Theory, volume 3170 of Lecture Notes in Computer Science, p35-p48, Springer, 2004.
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかしながら、従来の正則モデル検査では、有限オートマトンに対して繰り返し演算を行うため、有限オートマトンに係る演算の複雑さから、正則モデル検査が高速に行われないという問題があった。また、正則モデル検査に必要な、システム状態遷移規則の任意の回数の合成を表現する有限オートマトンを、有限オートマトン演算の繰り返しによって求めようとする場合、この繰り返しを何回行っても、繰り返しの結果求められる有限オートマトンが、繰り返しの回数に比例する回数以上のシステム状態遷移規則の合成を表すことができないため、このシステム状態遷移規則の任意の回数の合成を表現する有限オートマトンを求める計算が終了しないという問題があった。
【０００５】
本発明は、上記問題を解決すべくなされたもので、その目的は、コンピュータシステムの安全性検査を高速に行い、かつ有限の時間内で検査を終了させることを可能とする安全性検査方法、安全性検査装置及びコンピュータプログラム並びに記録媒体を提供することにある。
【課題を解決するための手段】
【０００６】
上記問題を解決するために、本発明は、コンピュータシステムの状態を有限文字集合の文字列で表現する有限オートマトンの情報に基づいて、前記コンピュータシステムの安全性を判定する安全性検査方法であって、前記コンピュータシステムの状態を示す状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、前記コンピュータシステムが安全でない状態を示す集合の情報と、前記コンピュータシステムの状態遷移の任意の回数の繰り返しを表現するオートマトンを有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力して記憶手段へ記録するステップと、前記記憶手段から前記システム状態遷移規則の情報と、前記拡張情報とを読み出し、読み出した前記システム状態遷移規則の情報と、前記拡張情報とに基づいて、前記局所言語を算出するステップと、算出した前記局所言語を用いて前記コンピュータシステムの状態遷移規則の任意の回数の合成を近似的に表す第２の有限オートマトンの情報を生成して出力するステップと、前記記憶手段から前記初期状態の集合の情報と前記安全でない状態を示す集合の情報とを読み出すステップと、読み出した前記初期状態の集合の情報と、前記安全でない状態を示す集合の情報と、前記第２の有限オートマトンの情報と、に基づいて安全性の判定を行うステップと、判定された安全であるか、あるいは安全でないかを示す判定結果を出力するステップと、を含むことを特徴とする安全性検査方法である。
【０００７】
本発明は、コンピュータシステムの状態を有限文字集合の文字列で表現する有限オートマトンの情報に基づいて、前記コンピュータシステムの安全性を判定する安全性検査装置であって、前記コンピュータシステムの状態を示す状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、前記コンピュータシステムが安全でない状態を示す集合の情報と、前記コンピュータシステムの状態遷移の任意の回数の繰り返しを表現するオートマトンを有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力して記憶手段へ記録する入力手段と、前記記憶手段から前記システム状態遷移規則の情報と、前記拡張情報とを読み出し、読み出した前記システム状態遷移規則の情報と、前記拡張情報とに基づいて、前記局所言語を算出し、算出した前記局所言語を用いて前記コンピュータシステムの状態遷移規則の任意の回数の合成を近似的に表す第２の有限オートマトンの情報を生成して出力する極限計算手段と、前記記憶手段から前記初期状態の集合の情報と前記安全でない状態を示す集合の情報とを読み出し、読み出した前記初期状態の集合の情報と、前記安全でない状態を示す集合の情報と、前記第２の有限オートマトンの情報と、に基づいて安全性の判定を行う安全性判定手段と、前記安全性判定手段によって判定された安全であるか、あるいは安全でないかを示す判定結果を出力する出力手段と、を備えたことを特徴とする安全性検査装置である。
【０００８】
本発明は、コンピュータシステムの状態を有限文字集合の文字列で表現する有限オートマトンの情報に基づいて、前記コンピュータシステムの安全性を判定する安全性検査装置のコンピュータに、前記コンピュータシステムの状態を示す状態集合の情報及び初期状態の集合の情報及びシステム状態遷移規則の情報と、前記コンピュータシステムが安全でない状態を示す集合の情報と、前記コンピュータシステムの状態遷移の任意の回数の繰り返しを表現するオートマトンを有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力して記憶手段へ記録するステップと、前記記憶手段から前記システム状態遷移規則の情報と、前記拡張情報とを読み出し、読み出した前記システム状態遷移規則の情報と、前記拡張情報とに基づいて、前記局所言語を算出するステップと、算出した前記局所言語を用いて前記コンピュータシステムの状態遷移規則の任意の回数の合成を近似的に表す第２の有限オートマトンの情報を生成して出力するステップと、前記記憶手段から前記初期状態の集合の情報と前記安全でない状態を示す集合の情報とを読み出すステップと、読み出した前記初期状態の集合の情報と、前記安全でない状態を示す集合の情報と、前記第２の有限オートマトンの情報と、に基づいて安全性の判定を行うステップと、判定された安全であるか、あるいは安全でないかを示す判定結果を出力するステップと、を実行させるためのコンピュータプログラムである。
【０００９】
本発明は、上記に記載のコンピュータプログラムを記録したコンピュータ読み取り可能な記録媒体である。
【発明の効果】
【００１０】
この発明によれば、コンピュータシステムの状態を示す状態集合の情報及びシステム状態遷移規則の情報と、安全性の判定に用いられる安全でない状態を示す集合の情報と、システム状態遷移規則の任意の回数の繰り返しを示す情報を有限の計算時間で算出することができる局所言語を算出するための拡張情報とを入力する。また、入力される状態集合の情報と、拡張情報とに基づいて、局所言語を算出する。そして、算出した局所言語を用いて、コンピュータシステムの状態遷移規則の任意の回数の繰り返しを示す第２の有限オートマトンの情報を生成して出力する構成とした。これにより、生成した第２の有限オートマトンに基づいて安全性検査を行うことが可能になる。また、局所言語を用いてシステム状態遷移規則の任意の回数の繰り返しを示す第２の有限オートマトンの情報を生成することにより、有限オートマトンの演算の繰り返しにより生成する場合よりも演算量を削減することができる。また、有限オートマトン演算の繰り返しにより生成する場合に生じることがある、システム状態遷移規則の任意の回数の繰り返しを示す第２の有限オートマトンの生成の計算が終了しない場合が、局所言語を用いて生成する場合には生じず、有限の計算時間で生成することができる。
【発明を実施するための最良の形態】
【００１１】
以下、本発明の一実施形態について図面を参照して説明する。
図１は、本実施形態に係る安全性検査装置１を示す概略ブロック図である。
図１において、入力部１０は、コンピュータシステム（以下、システムと記載）の初期状態の集合Ｉの情報、システムが安全でない状態の集合Ｐの情報、システム全体の状態遷移を示す状態遷移規則（以下、システム状態遷移規則と記載）Ｔの情報及び、局所言語を算出するためのシステム状態遷移規則Ｔの拡張情報を入力する。記憶部２０は、入力部１０により入力される情報を記憶する。極限計算部３０は、状態遷移規則Ｔ及びＴの拡張情報を記憶部２０から読み出し、読み出したシステム状態遷移規則Ｔ及びＴの拡張情報に基づいて、システムを局所言語で表現し、システムの任意の回数の状態遷移を表す規則（後述するＴ＜ω）の近似値を算出する。安全性判定部４０は、初期状態の集合Ｉ及び安全性集合Ｐを記憶部２０から読み出し、読み出した初期状態の集合Ｉ及び安全性集合Ｐと、Ｔ＜ωの近似値とに基づいてシステムの安全性を判定する。出力部５０は、安全性判定部４０により判定されたシステムの安全性の判定結果を出力する。
【００１２】
（安全性検査）
ここで、システムの安全性検査について説明する。システムの安全性検査は、次のように定式化して表現することができる。すなわち、システムは集合Ｓ、集合Ｉ及び規則Ｔの３つの組（Ｓ，Ｉ，Ｔ）によって表現することができる。集合Ｓは、システムの取り得る状態の集合である。集合Ｉは、集合Ｓの要素のうち、システムの初期状態である要素の集合であり、集合Ｓの部分集合である。規則Ｔは、システム状態遷移規則であり、集合Ｓの直積集合Ｓ×Ｓの部分集合である。このとき、状態ｓと状態ｓ’の２つの組（ｓ，ｓ’）がＴの要素であるとき、（ｓ，ｓ’）は、システムが１回の状態遷移によって状態ｓから次状態ｓ’に遷移することを示すこととなる。また、システムのｎ回の状態遷移を表す規則をＴｎで示した場合Ｔは帰納的に下記の式（１）によって表される。
【００１３】
【数１】
2007004236.tif 000003
【００１４】
式（１）の上段の式において、ｉｄは恒等関数である。式（１）下段の式の右辺は、システム状態遷移規則Ｔ及びＴｎの合成を示す式である。また、システムのｎ回以下の状態遷移を示す規則をＴ≦ｎと記載し、当該Ｔ≦ｎは、次式（２）により帰納的に定義される。
【００１５】
【数２】
2007004236.tif 000004
【００１６】
また、システムの任意の回数の状態遷移を表現する規則をＴ＜ωと記載し、当該Ｔ＜ωは、次式（３）により定義される。
【００１７】
【数３】
2007004236.tif 000005
【００１８】
次に、安全でない状態の集合をＰとする。上記のＳはＰの部分集合となる。集合Ｐをシステムの安全性集合とすると、このとき、システムが安全であるとは次式（４）を満たすこととなる。
【００１９】
【数４】
2007004236.tif 000006
【００２０】
式（４）において、φは空集合であり、安全性集合Ｐとの共通部分が空集合になるということは、安全でない状態が含まれず、システムが安全であるということを示すことになる。ここで、式（４）のＴ＜ω（Ｉ）は、システム状態遷移規則Ｔ＜ωの集合Ｉへの適用を示している。一般に、システムが有限オートマトンで表現される場合の集合Ｓ上の状態遷移規則（以下、有限オートマトン状態遷移規則と記載）ＲのＳの部分集合Ｘへの適用は次式（５）によって定義される。
【００２１】
【数５】
2007004236.tif 000007
【００２２】
（正則モデル検査）
次に、有限オートマトンを正則言語としてシステムを表現した場合、当該システムに対して上記の安全性検査を行う場合に適用される正則モデル検査について説明する。正則モデル検査では、次の条件を満たすシステムを対象としている。
（１）状態集合Ｓは、文字の有限集合（以下、有限文字集合と記載）Σを用いてΣ＊で表現される集合である。ここで、Σ＊は、Σの文字からなる文字列の集合である。
（２）初期状態の集合Ｉは、Σ上の正則言語である。
（３）安全性集合Ｐは、Σ上の正則言語である。
（４）状態遷移規則Ｔは、Σ×Σ上の正則言語で表現される。
【００２３】
Σ×Σ上の正則言語の要素（ａ１，ａ１’）…（ａｎ，ａｎ’）を、Σ＊×Σ＊の要素（ａ１…ａｎ，ａ１’…ａｎ’）と同一視することにより、Σ×Σ上の正則言語をΣ＊上の状態遷移規則とみなすことができる。
【００２４】
このとき、図２に示す手順にて正則モデル検査が実行される。なお、図２に示す手順は、本発明の実施形態に係る局所言語を正則言語とした場合の処理との対比のため、本実施形態に係る安全性検査装置１００の構成を参照して説明を行う。既に入力部１０により初期状態の集合Ｉの情報、安全性集合Ｐの情報、システム状態遷移規則Ｔの情報が入力され、記憶部２０に記憶されているものとする。まず最初に、極限計算部３０が、記憶部２０から状態遷移規則Ｔを読み出し、読み出した状態遷移規則Ｔに基づいて、Ｔ＜ωを算出し、算出したＴ＜ωを安全性判定部４０に入力する（ステップＳａ１）。次に、安全性判定部４０は、記憶部２０から初期状態の集合Ｉと、安全性集合Ｐを読み出し、上記の式（４）の演算を行う。そして、安全性判定部４０は、演算結果が空集合φであるなら安全として出力部５０に出力させ、空集合φでないなら安全でないとして出力部５０に出力させる（ステップＳａ２）。
【００２５】
（局所言語を用いた正則モデル検査）
次に、本発明の実施形態に係る安全性検査装置１００により行われる安全性検査に適用される正則モデル検査について説明する。上記の有限オートマトンを正則言語とした正則モデル検査では、極限計算部３０が状態遷移規則Ｔに基づいて有限オートマトンに基づく演算によりシステムの任意の回数の状態遷移を表す規則Ｔ＜ωを算出していた。本発明の実施形態に係る安全性検査装置１００では、有限オートマトンと同様に正則言語を表現することができる言語として知られている局所言語（例えば、A.Salomaa. Jewels of Formal Language Theory. Computer Science Press, p96-117, 1981参照）を用いて検査を行う。以下、図３及び図４を参照して安全性検査装置１００の動作について説明する。
【００２６】
図３に示す手順の前提として、既に入力部１０により初期状態の集合Ｉの情報、安全性集合Ｐの情報、システム状態遷移規則Ｔの情報に加えて、Ｔの拡張情報が入力され、記憶部２０に記憶されているものとする。
まず最初に、極限計算部３０が、記憶部２０からシステム状態遷移規則ＴとＴの拡張情報とを読み出し、読み出したシステム状態遷移規則ＴとＴの拡張情報とに基づいて、Ｔ＜ωの近似値を算出する。Ｔ＜ωの近似値は、図４に示す手順によって算出されるため、以下、図４を参照して詳細な手順について説明する。
【００２７】
（Ｓｃ１：Ｔの拡張情報を読み出すステップ）
図４において、まず最初に極限計算部３０が、記憶部２０からシステム状態遷移規則Ｔ及びＴの拡張情報を記憶部３０から読み出す。ここで、システム状態遷移規則Ｔを受理言語とするΣ×Σ上の有限オートマトンをＡＴと記載する。このとき、極限計算部３０が読み出したＴの拡張情報には、Σを包含する集合Σ’及び、Σ’とΣとの関係を示すΣ’からΣへの関数μが含まれている。ここで、関数μは、Σ’の要素ａに対し、ａがΣの要素であるならば、μ（ａ）はａに等しくなるような関数である。また、さらに、Ｔの拡張情報には、ＡＴを拡張したΣ’上の有限オートマトンＡＴ’の情報が含まれている。
【００２８】
以下に、有限オートマトンＡＴと有限オートマトンＡＴ’の関係について説明する。ＡＴ’において、状態集合、初期状態及び受理状態の集合はＡＴと同じである。このとき、ＡＴ’の任意の有限オートマトン状態遷移規則（ｑ，（ａ，ａ’），ｑ’）について、ＡＴの有限オートマトン状態遷移規則（ｑ，（μ（ａ），μ（ａ’）），ｑ’）が存在する。また、ＡＴの任意の有限オートマトン状態遷移規則（ｑ，（ａ，ａ’），ｑ’）について、ＡＴ’の有限オートマトン状態遷移規則（ｑ，（ｂ，ｂ’），ｑ’）のうち、μ（ｂ）及びμ（ｂ’）がそれぞれ、ａ及びａ’に等しいものが存在する。また、さらに、ＡＴ’の任意の有限オートマトン状態遷移規則（ｑ１，（ａ１，ａ１’），ｑ１’）および（ｑ２，（ａ２，ａ２’），ｑ２’）について、ｑ１’がｑ２’に等しいならば、ａ１とａ２とが異なるか、あるいはａ１’とａ２’とが異なるかのいずれかになるとする。
【００２９】
（Ｓｃ２：ＡＴ’を表現する局所言語を算出するステップ）
次に、極限計算部３０は、ＡＴ’を表現する局所言語Ｌを算出する。局所言語を算出するために、集合Ａ、Ｂ、Ｃを有限オートマトンＡＴの状態遷移規則Ｒと、有限オートマトンＡＴの受理状態の集合Ｆと、有限文字集合Σに基づいて、式（６）のように設定する。
【００３０】
【数６】
2007004236.tif 000008
【００３１】
このとき、局所言語Ｌ（Ａ，Ｂ，Ｃ）について、μ（Ｌ）＝Ｔという関係が成立する。
【００３２】
（Ｓｃ３：ＬからＬ’を算出するステップ）
次に、極限計算部３０は、局所言語ＬからＬ’を算出する。局所言語ＬからＬ’を算出するため、集合Ａｎを次式（７）ように帰納的に設定する。
【００３３】
【数７】
2007004236.tif 000009
【００３４】
また、同様に集合Ｂｎを次式（８）ように帰納的に設定する。
【００３５】
【数８】
2007004236.tif 000010
【００３６】
また、同様に集合Ｃｎを次式（９）ように帰納的に設定する。
【００３７】
【数９】
2007004236.tif 000011
【００３８】
Σは有限文字集合なので、Ａ１，Ａ２，Ａ３，…を計算すると、あるｎについてＡｎ＝Ａｎ＋１となる。このようなｎに対するＡｎをＡ’とし、同様にＢｎ＝Ｂｎ＋１となるＢｎをＢ’とし、Ｃｎ＝Ｃｎ＋１となるＣｎをＣ’とする。
これらのＡ’、Ｂ’及びＣ’から局所言語Ｌ’を算出する。このようにして算出された局所言語Ｌ’がＴ＜ωの近似値を表現できる局所言語となる。
【００３９】
（Ｓｃ４：Ｌ’からＡＬ’を算出するステップ）
次に、極限計算部３０は、局所言語Ｌ’から有限オートマトンＡＬ’を算出する。局所言語Ｌ’（Ａ’，Ｂ’，Ｃ’）からＡＬ’を算出するため、ＡＬ’の状態集合Ｑ’をΣ×Σ及び集合｛ｑ０’｝の和集合とする。ただし、ｑ０’はΣ×Σの要素でないとする。ここで、ＡＬ’の初期状態をｑ０’とし、ＡＬ’の受理状態の集合Ｆ’をＢ’とする。このとき、ＡＬ’に係る有限オートマトン状態遷移規則Ｒ’は次式（１０）により算出される。
【００４０】
【数１０】
2007004236.tif 000012
【００４１】
（Ｓｃ５：Ｔ＜ωの近似値を出力するステップ）
このようにして、有限オートマトンＡＬ’が初期状態をｑ０’、受理状態の集合Ｂ’、有限オートマトン状態遷移規則Ｒ’によって定義することができ、局所言語Ｌ’によって表現された有限オートマトンＡＬ’が算出される。この有限オートマトンＡＬ’がＴ＜ωの近似値、すなわちＡＬ’となり、極限計算部３０は、ＡＬ’をＴ＜ωの近似値として安全性判定部４０に入力する。
【００４２】
ここで、図３に戻り、安全性判定部４０は、記憶部２０から初期状態の集合Ｉと、安全性集合Ｐを読み出し、極限計算部３０により入力されたＴ＜ωの近似値に基づいて、上記の式（４）の演算を行う。そして、安全性判定部４０は、演算結果が空集合φであるなら安全として出力部５０に出力させ、空集合φでないなら安全でないとして出力部５０に出力させる（ステップＳｂ２）。
【００４３】
このようにして、システム状態遷移Ｔを、Ｔを表す有限オートマトンＡＴおよび拡張情報から、局所言語Ｌ’に表現し直すことで、Ｔの任意の回数の合成Ｔ＜ωを表すオートマトンＡＬ’を、これをＡＴから有限オートマトンの演算の繰り返しにより求める場合よりも少ない演算量で求めることが可能となる。
また、ＬからＬ’を算出するステップが有限回で必ず終了するためＴ＜ωを表すオートマトンＡＬ’を求める計算を、有限の時間内に終了させることが可能となる。つまり、ＡＴに対し有限オートマトンの演算を繰り返すことによりＴ＜ωを表すオートマトンを求める従来の方法では、ＬからＬ’を算出するステップに相当するステップの計算が有限時間内に終了しない状態が発生していたが、これは、有限オートマトンを用いて表現できる言語の種類が無限に存在することに起因していた。本実施形態では、局所言語を用いることにより、これを用いて表現できる言語の種類が有限となり、これによりＬからＬ’を算出するステップを有限時間内で実行することが可能となり、検証を有限時間内で終了させることが可能となる。
【００４４】
（実施例）
次に、上記の局所言語を適用した正則モデル検査に基づくシステムの安全性検査の具体的な実施例について図５を参照しつつ説明する。
図５は、実施例に係るコンピュータシステムの概略ブロック図である。当該コンピュータシステムでは、複数のコンピュータ１〜５が一列に並び、隣接するコンピュータのみが直接通信できるような接続され、当該接続によりネットワークが構成されている。当該コンピュータシステムにおいて、左側に隣接するコンピュータからトークンを受信し、受信したトークンを右側に隣接するコンピュータへ転送する通信処理が行われる。図５は、５つのコンピュータ１〜５が接続されており、最左のコンピュータ１から最右のコンピュータ５にトークンが順に転送される段階（第１〜第５段階）を示している。なお、図５において、コンピュータ１〜５のそれぞれを示す丸印の中の「ｔ」は、トークンを受信して内部に記憶している状態であり、「ｎ」はトークンを内部に記憶していない状態を示している。
【００４５】
図５のコンピュータシステムの状態は、Σ＝｛ｔ，ｎ｝を文字集合とする文字列で表現することができる。このとき、このシステム状態遷移規則Ｔを表す有限オートマトンＡＴは、以下のように定義することができる。すなわち、ＡＴの状態集合Ｑを｛ｑ０，ｑ１，ｑ２｝、ＡＴの初期状態をｑ０、ＡＴの受理状態の集合Ｆを｛ｑ２｝、ＡＴの有限オートマトン状態遷移規則Ｒを｛（ｑ０，（ｎ，ｎ），ｑ０），（ｑ０，（ｔ，ｎ），ｑ１），（ｑ１，（ｎ，ｔ），ｑ２），（ｑ２，（ｎ，ｎ），ｑ２）｝とする。
【００４６】
当該コンピュータシステムに対して、初期状態として最左のコンピュータ１からトークンを内部に記憶しており、それ以外のコンピュータ２〜５はトークンを記憶していない状態とする。初期状態の集合Ｉは、ｔｎｎ…という構成の文字列の集合となる。また、安全でない状態を、トークンを２つ以上のコンピュータが同時に内部に記憶する状態とする。そのとき、安全でない状態の集合Ｐは、Ｐが…ｎ…ｎｔｎ…ｎｔｎ…のようにｔが２回以上出現する文字列の集合となる。
【００４７】
ここで、上記のコンピュータシステムに、上述した安全性検査装置１００を適用した場合に、安全性検査装置１００の極限計算部３０によって行われるＴ＜ωの近似値を算出する過程を、図４のフローチャートの流れに従って説明する。
【００４８】
（Ｓｃ１：Ｔの拡張情報を読み出すステップ）
入力部１０により入力され、記憶部２０に記憶されるＴの拡張情報を読み出す。当該Ｔの拡張情報にはΣ’としてΣ∪｛ｎ’｝が含まれている。また、当該Ｔの拡張情報にはμ（ｎ’）＝ｎとなるμが含まれている。また、さらに、当該Ｔの拡張情報には有限オートマトン状態遷移規則Ｒが｛（ｑ０，（ｎ，ｎ），ｑ０），（ｑ０，（ｔ，ｎ），ｑ１），（ｑ１，（ｎ’，ｔ），ｑ２），（ｑ２，（ｎ’，ｎ’），ｑ２）｝であるＡＴ’が含まれている。
【００４９】
（Ｓｃ２：ＡＴ’を表現する局所言語を算出するステップ）
局所言語Ｌを算出するための集合Ａ、Ｂ及びＣは、次式（１１）によって示される。
【００５０】
【数１１】
2007004236.tif 000013
【００５１】
（Ｓｃ３：ＬからＬ’を算出するステップ）
式（１１）によって示される集合Ａ、Ｂ及びＣから局所言語Ｌ’を算出するための集合Ａ’、Ｂ’及びＣ’は、次式（１２）によって示される。
【００５２】
【数１２】
2007004236.tif 000014
【００５３】
（Ｓｃ４：Ｌ’からＡＬ’を算出するステップ）
有限オートマトンＡＬ’を定義する局所言語Ｌ’によって表現された有限オートマトン状態遷移規則Ｒ’は次式（１３）によって示される。
【００５４】
【数１３】
2007004236.tif 000015
【００５５】
（Ｓｃ５：Ｔ＜ωの近似値を出力するステップ）
このようにして、有限オートマトンＡＬ’を初期状態をｑ０’、受理状態の集合Ｂ’、有限オートマトン状態遷移規則Ｒ’により定義することができ、局所言語Ｌ’によって表現された有限オートマトンＡＬ’が算出される。この有限オートマトンＡＬ’がＴ＜ωの近似値となり、極限計算部３０は、ＡＬ’をＴ＜ωの近似値として安全性判定部４０に入力する。
【００５６】
安全性判定部４０は、極限計算部３０から入力されるＡＬ’と、記憶部２０から読み出す初期状態の集合Ｉ及び安全でない状態の集合Ｐを表す有限オートマトンＡＩ及びＡＰを生成し、次式（１４）が成り立つか否かにより安全性の判定を行う。
【００５７】
【数１４】
2007004236.tif 000016
【００５８】
ここで、初期状態の集合Ｉを表す有限オートマトンＡＩは、状態集合ＱＩ＝｛ｑ０，ｑ１｝、初期状態ｑ０、受理状態の集合Ｆ＝｛ｑ１｝及び有限オートマトン状態遷移規則ＲＩ＝｛（ｑ０，ｔ，ｑ１），（ｑ１，ｎ，ｑ１）｝によって定義される有限オートマトンとなる。また、安全でない状態の集合Ｐを表す有限オートマトンＡＰは、状態集合Ｑｐ＝｛ｑ０，ｑ１，ｑ２｝、初期状態ｑ０、受理状態の集合Ｆ＝｛ｑ２｝及び次式（１５）により示される有限オートマトン状態遷移規則Ｒｐによって定義される有限オートマトンとなる。
【００５９】
【数１５】
2007004236.tif 000017
【００６０】
なお、別紙特許請求の範囲に記載の、システム初期状態の集合は、システムの初期状態の集合Ｉに対応し、システムが安全でない状態を示す集合は、集合Ｐに対応し、システム状態遷移規則は、システム状態遷移規則Ｔに対応し、局所言語を算出するための拡張認証は、Ｔの拡張情報に対応する。また、第２の有限オートマトンは、有限オートマトンＡＬ’に対応する。
【００６１】
上述の安全性検査装置は内部に、コンピュータシステムを有している。そして、上述した安全性検査及び正則モデル検査の処理は、プログラムの形式でコンピュータ読み取り可能な記録媒体に記憶されており、このプログラムをコンピュータが読み出して実行することによって、上記処理が行われる。ここでコンピュータ読み取り可能な記録媒体とは、磁気ディスク、光磁気ディスク、ＣＤ−ＲＯＭ、ＤＶＤ−ＲＯＭ、半導体メモリ等をいう。また、このコンピュータプログラムを通信回線によってコンピュータに配信し、この配信を受けたコンピュータが当該プログラムを実行するようにしても良い。
【図面の簡単な説明】
【００６２】
【図１】本実施形態に係る安全性検査装置の内部構成を示すブロック図である。
【図２】正則言語として有限オートマトンを用いた場合の安全性検査処理の流れを示したフローチャートである。
【図３】本実施形態に係る正則言語として局所言語を用いた場合の安全性検査処理の流れを示したフローチャートである。
【図４】本実施形態に係る極限計算部による処理を示したフローチャートである。
【図５】本実施形態に係る安全性検査装置が適用される実施例による安全性検査を説明するための図である。
【符号の説明】
【００６３】
１０  入力部
２０  記憶部
３０  極限計算部
４０  安全性判定部
５０  出力部
１００  安全性検査装置
【図１】
2007004236.tif 000018
【図２】
2007004236.tif 000019
【図３】
2007004236.tif 000020
【図４】
2007004236.tif 000021
【図５】
2007004236.tif 000022