(57)【要約】【課題】２つのオートマトン間の対応関係を、一致の尤度が高くなるように推定する状態遷移対応推定装置及び状態遷移対応推定方法を提供する。【解決手段】一実施形態に係る状態遷移対応推定装置は、作成部と、求解部と、抽出部とを備える。作成部は、複数の状態と状態間の状態遷移とをそれぞれ含む第１のオートマトン及び第２のオートマトンの対応関係を示す論理式を、第２のオートマトンが第１のオートマトンを模倣するという前提で作成する。求解部は、真になる節が最大となる論理式の解を求める。抽出部は、解に基づいて、対応関係を抽出する。【選択図】図１
2016057978.tif 000002
【特許請求の範囲】
【請求項１】
複数の状態と前記状態間の状態遷移とをそれぞれ含む第１のオートマトン及び第２のオートマトンの対応関係を示す論理式を、前記第２のオートマトンが前記第１のオートマトンを模倣するという前提で作成する作成部と、
真になる節が最大となる前記論理式の解を求める求解部と、
前記解に基づいて、前記対応関係を抽出する抽出部と、
を備える状態遷移対応推定装置。
【請求項２】
前記作成部は、前記第１のオートマトンに含まれる前記状態と、前記第２のオートマトンに含まれる前記状態と、の組である状態対を変数として含む前記論理式を作成する
請求項１に記載の状態遷移対応推定装置。
【請求項３】
前記作成部は、前記第１のオートマトンに含まれる遷移元の状態ｐ及び遷移先の状態ｐ′と、前記第２のオートマトンに含まれる遷移元の状態ｑ及び遷移先の状態ｑ′と、に関して、
前記状態ｐと前記状態ｑとが対応する場合、前記状態ｐ′と前記状態ｑ′とが対応する、ということを示す節を含む前記論理式を作成する
請求項１又は請求項２に記載の状態遷移対応推定装置。
【請求項４】
前記求解部は、前記論理式の前記解として、前記状態ｐと前記状態ｑとが対応する場合、前記状態ｐ′と前記状態ｑ′とが対応する、ということを示す前記節をソフト節として含むPartial Max-Sat問題の解を求める
請求項３に記載の状態遷移対応推定装置。
【請求項５】
前記抽出部は、前記解に含まれる前記変数の値に基づいて、前記第１のオートマトンの前記状態と、前記第２のオートマトンの前記状態と、の対応関係を抽出する
請求項１〜請求項４のいずれか１項に記載の状態遷移対応推定装置。
【請求項６】
前記抽出部は、前記論理式と前記解とに基づいて、前記第１のオートマトンの前記状態遷移と、前記第２のオートマトンの前記状態遷移と、の対応関係を抽出する
請求項１〜請求項５のいずれか１項に記載の状態遷移対応推定装置。
【請求項７】
対応する前記状態対及び対応しない前記状態対の少なくとも一方を予め設定される
請求項１〜請求項６のいずれか１項に記載の状態遷移対応推定装置。
【請求項８】
前記第１のオートマトンは、システムの仕様から生成されたオートマトンであり、
前記第２のオートマトンは、前記システムのソースコードから生成されたオートマトンである
請求項１〜請求項７のいずれか１項に記載の状態遷移対応推定装置。
【請求項９】
複数の状態と前記状態間の状態遷移とをそれぞれ含む第１のオートマトン及び第２のオートマトンの対応関係を示す論理式を、前記第２のオートマトンが前記第１のオートマトンを模倣するという前提で作成し、
真になる節が最大となる前記論理式の解を求め、
前記解に基づいて、前記対応関係を抽出する
ことを含む状態遷移対応推定方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、状態遷移対応推定装置及び状態遷移対応推定方法に関する。
【背景技術】
【０００２】
仕様書に基づいてシステムを構築する際、システムに実装されたソースコードが仕様書で定めた仕様に従って動作するかを判定するために、仕様書から生成したオートマトン（状態機械）と、ソースコードから生成したオートマトンとを比較する方法が知られている。しかしながら、仕様書とソースコードとは抽象度や記述者が違うことが多い。またいずれか一方あるいは両方が誤りを含むことがある。このため、システムのソースコードから生成したオートマトンと、システムの仕様書から生成したオートマトンとは、必ずしも完全に対応するとは限らず、両者の対応関係を機械的に抽出することは困難であった。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００８−２６９５８５号公報
【特許文献２】特開２００６−２４１７９号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
２つのオートマトン間の対応関係を、一致の尤度が高くなるように推定する状態遷移対応推定装置及び状態遷移対応推定方法を提供する。
【課題を解決するための手段】
【０００５】
一実施形態に係る状態遷移対応推定装置は、作成部と、求解部と、抽出部とを備える。作成部は、複数の状態と状態間の状態遷移とをそれぞれ含む第１のオートマトン及び第２のオートマトンの対応関係を示す論理式を、第２のオートマトンが第１のオートマトンを模倣するという前提で作成する。求解部は、真になる節が最大となる論理式の解を求める。抽出部は、解に基づいて、対応関係を抽出する。
【図面の簡単な説明】
【０００６】
【図１】状態遷移対応推定装置の機能構成を示すブロック図。
【図２】図１の変形例を示すブロック図。
【図３】状態遷移対応推定装置のハードウェア構成を示すブロック図。
【図４】状態遷移対応推定装置の動作を示すフローチャート。
【図５】上位オートマトンの一例を示す状態遷移図。
【図６】下位オートマトンの一例を示す状態遷移図。
【図７】表示装置に表示される状態遷移図の一例を示す図。
【図８】表示装置に表示される対応状態対及び不対応状態対の一例を示す図。
【図９】表示装置に表示される対応状態対及び不対応状態対の他の例を示す図。
【図１０】対応可能状態対の作成処理を示すフローチャート。
【図１１】表示装置に表示される対応可能状態対、対応状態対、及び不対応状態対の一例を示す図。
【図１２】論理式の作成処理を示すフローチャート。
【図１３】集合C，Dに含まれる節を示す図。
【図１４】対応関係の抽出処理を示すフローチャート。
【図１５】表示装置に表示される状態間の対応関係の一例を示す図。
【図１６】表示装置に表示される状態間の対応関係の他の例を示す図。
【図１７】表示装置に表示される状態遷移間の対応関係の一例を示す図。
【発明を実施するための形態】
【０００７】
以下、本発明の実施形態に係る状態遷移対応推定装置及び状態遷移対応推定方法について図面を参照して説明する。
【０００８】
（第１実施形態）
まず、状態推移対応推定装置（以下、「推定装置」という）の機能構成について、図１〜図２を参照して説明する。図１は、推定装置の機能構成を示すブロック図である。図１に示すように、この推定装置は、上位オートマトン記憶部１と、下位オートマトン記憶部２と、状態対応記憶部３と、論理式作成部４と、論理式記憶部５と、論理式求解部６と、解記憶部７と、対応関係抽出部８と、対応関係記憶部９とを備える。
【０００９】
上位オートマトン記憶部１は、上位オートマトン（第１のオートマトン）を記憶する。上位オートマトンは、複数の状態と、各状態間の状態遷移とを含むオートマトンである。状態遷移は、２つの状態の順序付きペアにより構成される。状態遷移の一方の状態は、遷移元の状態を示し、他方の状態は遷移先の状態を示す。上位オートマトンは、例えば、システムの仕様書から生成されたオートマトンであるが、これに限られない。上位オートマトンは、推定装置のユーザにより入力され、記憶される。
【００１０】
下位オートマトン記憶部２は、下位オートマトン（第２のオートマトン）を記憶する。下位オートマトンは、複数の状態と、各状態間の状態遷移とを含むオートマトンである。状態遷移は、２つの状態の順序付きペアにより構成される。状態遷移の一方の状態は、遷移元の状態を示し、他方の状態は遷移先の状態を示す。下位オートマトンは、例えば、システムのソースコードから生成されたオートマトンであるが、これに限られない。下位オートマトンは、推定装置のユーザにより入力され、記憶される。
【００１１】
或いは、下位オートマトンは、ソースコードを解析してオートマトンを生成する既存の技術を用いて生成され、記憶されてもよい。オートマトンを生成する技術として、例えば、以下の文献に記載の方法が知られている。
Enabledness-based program abstractions for behavior validation
Guido De Caso, Victor Braberman, Diego Garbervetsky, Sebastian Uchitel      (2013)
ACM Transactions on Software Engineering and Methodology      22 (3)        p. 1
【００１２】
このような技術を用いて下位オートマトンを生成する場合、推定装置は、図２に示すように、ソースコードから下位オートマトンを生成する下位オートマトン生成部１０を更に備える。この場合、ユーザは、下位オートマトンのかわりにソースコードを入力する。下位オートマトン生成部１０は、ユーザにより入力されたソースコードを解析して下位オートマトンを生成する。生成された下位オートマトンは、下位オートマトン記憶部２に記憶される。
【００１３】
なお、上位オートマトン及び下位オートマトンには、状態遷移を発生させるイベントを示すラベルが含まれてもよい。この場合、状態遷移は、遷移元の状態と、遷移先の状態と、ラベルとにより構成される。ラベルを含むオートマトンが生成されるシステムは、ラベル付き遷移システムと称される。
【００１４】
状態対記憶部３は、対応状態対及び不対応状態対の少なくとも一方を記憶する。状態対とは、上位オートマトンに含まれる状態と、下位オートマトンに含まれる状態との対である。対応状態対は、２つの状態が対応する状態対である。不対応状態対は、２つの状態が対応しない状態対である。対応状態対及び不対応状態対は、推定装置のユーザにより予め設定され、状態対記億部３に記憶される。なお、推定装置は、状態対記憶部３を備えない構成も可能である。
【００１５】
論理式作成部４は、上位オートマトン記憶部１に記憶された上位オートマトンと、下位オートマトン記憶部２に記憶された下位オートマトンと、状態対応記憶部３に記憶された対応状態対及び不対応状態対と、に基づいて、上位オートマトンと下位オートマトンとの対応関係を示す論理式を作成する。
【００１６】
論理式作成部４は、上位オートマトンと下位オートマトンとの間に実際に模倣関係が成り立つか否かに関わらず、下位オートマトンが上位オートマトンを模倣するという前提で作成する。
【００１７】
模倣関係とは、２つのオートマトンの間に成り立つ関係であり、任意のイベントに対して、一方のオートマトンが他方のオートマトンと外観的に等価に振る舞うことを保証された関係のことである。ここで、Sをオートマトンに含まれる状態の集合、Dをオートマトンに含まれる状態遷移の集合とすると、２つのオートマトンM1=＜S1，D1＞，M2＝＜S2，D2＞に関して、模倣関係は以下のように定義される。
【００１８】
模倣関係：R＝S×S
s∈S1，t∈S2に対して(s，t)∈Rならば、
任意のs′∈S1，(s，s′)∈D1に対して
t′∈S2，(t，t′)∈D2が存在して
(s′，t′)∈Rが成り立つ。
このとき、M1≦RM2と表され、「M2はM1を模倣する」という。
【００１９】
以下では、上位オートマトンに含まれる遷移元の状態をp、状態pからの遷移先の状態（後続状態）をp′、状態pから状態p′への状態遷移を(p，p′)、下位オートマトンに含まれる遷移元の状態をq、状態qからの遷移先の状態（後続状態）をq′、状態qから状態q′への状態遷移を(q，q′)、状態pと状態qとからなる状態対をp−qと表す。上位オートマトンと下位オートマトンとの間に模倣関係が成立する場合、任意のp，q，p′，q′に対して、¬Xp,q∨Xp′,q′が成り立つ。Xp,qは状態対p−qの真理値を示す変数である。Xp,qが真とは、状態pと状態qとが対応することを示し、Xp,qが偽とは、状態pと状態qとが対応しないことを示す。
【００２０】
¬Xp,q∨Xp′,q′は、状態pと状態qとが対応する（状態対p−qが対応状態対である）場合、状態p′と状態q′とが対応する（状態対p′−q′が対応状態対である）ことを示している。論理式は、下位オートマトンが上位オートマトンを模倣するという前提で作成されるため、任意のp，q，p′，q′に対する¬Xp,q∨Xp′,q′を節として含む論理積となる。
【００２１】
状態pの後続状態p′や、状態qの後続状態q′が複数ある場合、Xp,qに対応するXp′,q′は複数存在する。このような場合には、複数存在する任意のXpm′,qn′に関して、Xp′,q′＝∨Xpm′,qn′であるものとする。
【００２２】
なお、Xp,qが対応状態対として設定されている場合、Xp,qは真であるため、論理式の節として、¬Xp,q∨Xp′,q′以外にXp,qも追加される。Xp,qが不対応状態対として設定されている場合、Xp,qは偽、すなわち、¬Xp,qは真であるため、論理式の節は¬Xp,qとされ、¬Xp,q∨Xp′,q′は常に成り立つため省かれる。論理式作成部４により作成された論理式は、論理式記憶部５に記憶される。
【００２３】
論理式求解部６は、論理式記憶部５に記憶された論理式の解を求める。この際、論理式求解部６は、論理式に含まれる節のうち、真となる節が最大となるように、解を求める。より詳細には、真となる¬Xp,q∨Xp′,q′の数が最大となるように解を求める。論理式求解部６により求められる解は、任意のp，qに対する変数Xp,q＝１又は０の集合となる。以下の説明において、真を１で表し、偽を０で表す。
【００２４】
上位オートマトンと下位オートマトンとが完全に対応し、模倣関係が成立している場合、論理式の全ての節が真となる解を得られるが、実際には、模倣関係が成立しているとは限らない。しかしながら、上記のように論理式の解を求めることにより、模倣関係が最大限成立する解、すなわち、上位オートマトンと下位オートマトンとの対応関係の一致の尤度が最大となる解を得ることができる。
【００２５】
上記の論理式は、¬Xp,q∨Xp′,q′をソフト節として含み、Xp,q及び¬Xp,qをハード節として含む、いわゆるPartial Max-Sat問題である。したがって、論理式求解部６は、線形計画法などの、Partial Max-Sat問題の任意の解法を用いて解を求めることができる。論理式求解部６により求められた解は、解記憶部７に記憶される。
【００２６】
対応関係抽出部８は、解記憶部７に記憶された解に基づいて、上位オートマトンと下位オートマトンとの対応関係を抽出する。すなわち、論理式の解から、状態及び状態遷移の対応関係をデコードする。
【００２７】
状態の対応関係は、各変数Xp,qの値から抽出することができる。Xp,q＝１の場合、上位オートマトンの状態qと、下位オートマトンの状態qとは対応する（状態対p−qは対応状態対である）。Xp,q＝０の場合、上位オートマトンの状態qと、下位オートマトンの状態qとは対応しない（状態対p−qは不対応状態対である）。
【００２８】
また、状態遷移の対応関係は、各変数Xp,qの値を論理式の各節に代入することにより抽出することができる。¬Xp,q∨Xp′,q′＝１の場合、(p，p′)と(q，q′)とは対応する。¬Xp,q∨Xp′,q′＝０の場合、(p，p′)と(q，q′)とは対応しない。対応関係抽出部８により抽出された対応関係は、対応関係記憶部９に記憶される。
【００２９】
次に、推定装置のハードウェア構成について、図３を参照して説明する。図３は、状態推定装置のハードウェア構成を示すブロック図である。図３に示すように、推定装置は、コンピュータ装置１００により構成される。このコンピュータ装置１００は、ＣＰＵ１０１と、入力装置１０２と、表示装置１０３と、通信装置１０４と、主記憶装置１０５と、外部記憶装置１０６とを備え、これらはバス１０７により相互に接続されている。
【００３０】
ＣＰＵ（中央演算装置）１０１は、主記憶装置１０５上で、状態遷移対応推定プログラム（以下、「推定プログラム」という）を実行する。推定プログラムとは、推定装置の上述の各機能構成を実現するプログラムのことである。ＣＰＵ１０１が、推定プログラムを実行することにより、各機能構成は実現される。
【００３１】
入力装置１０２は、推定装置に外部からデータや命令を入力するための装置である。入力装置１０２は、例えば、キーボード、マウス、及びタッチパネルなどの、ユーザが直接的に入力するための装置であってもよい。また、入力装置１０２は、外部装置からの入力を可能にするＵＳＢなどの装置や、ソフトウエアであってもよい。上位オートマトン、下位オートマトン、対応状態対、及び不対応状態対などの情報は、この入力装置１０２を介して推定装置に入力することができる。
【００３２】
表示装置１０３は、推定装置から出力される映像信号を表示するディスプレイである。表示装置は、例えば、ＬＣＤ（液晶ディスプレイ）、ＣＲＴ（ブラウン管）、及びＰＤＰ（プラズマディスプレイ）であるが、これに限られない。上位オートマトン、下位オートマトン、対応状態対、不対応状態対、及び対応関係抽出部により抽出された対応関係などの情報は、この表示装置１０３により表示することができる。
【００３３】
通信装置１０４は、推定装置が外部装置と通信するための装置である。推定装置は、通信装置１０４を介して、外部装置と所定の通信方式で無線通信又は有線通信を行う。通信装置１０４は、例えば、モデムやルータであるが、これに限られない。上位オートマトン、下位オートマトン、対応状態対、及び不対応状態対などの情報は、この通信装置１０４を介して外部装置から入力されてもよい。
【００３４】
主記憶装置１０５は、推定プログラムの実行の際に、推定プログラム、推定プログラムの実行に必要なデータ、及び推定プログラムの実行により生成されたデータなどを記憶する。推定プログラムは、主記憶装置１０５上で展開され、実行される。主記憶装置１０５は、例えば、ＲＡＭ、ＤＲＡＭ、ＳＲＡＭであるが、これに限られない。上位オートマトン記憶部１、下位オートマトン記憶部２、状態対記億部３、論理式記憶部５、解記憶部７、及び対応関係記憶部９は、この主記憶装置１０５上及び外部記憶装置１０６上の少なくとも一方に構築される。また、主記憶装置１０５は、コンピュータ装置１００のＯＳ、ＢＩＯＳ、及び各種のミドルウエアを記憶してもよい。
【００３５】
外部記憶装置１０６は、推定プログラム、推定プログラムの実行に必要なデータ、及び推定プログラムの実行により生成されたデータなどを記憶する。これらのプログラムやデータは、推定プログラムの実行の際に、主記憶装置１０５に読み出される。外部記憶装置１０６は、例えば、ハードディスク、光ディスク、フラッシュメモリ、及び磁気テープであるが、これに限られない。
【００３６】
なお、推定プログラムは、コンピュータ装置１００に予めインストールされていてもよいし、ＣＤ−ＲＯＭなどの記憶媒体に記憶されていてもよい。また、推定プログラムは、インターネット上にアップロードされていてもよい。
【００３７】
次に、推定装置の動作について、具体例を用いて詳細に説明する。以下では、上位オートマトンは、システムの仕様書から生成されたオートマトンであり、下位オートマトンは、仕様書に基づいて実装されたソースコードから生成されたオートマトンであるものとする。また、上位オートマトン及び下位オートマトンはいずれもユーザにより入力されるものとする。ここで、図４は、推定装置の動作を示すフローチャートである。
【００３８】
ステップＳ１において、上位オートマトン記憶部１は、ユーザにより入力された上位オートマトンを記憶する。図５は、上位オートマトンを示す状態遷移図である。図５において、符号付きの丸印は状態を示しており、矢印は状態遷移を示している。矢印の元の状態は遷移元の状態であり、矢印の先の状態は遷移先の状態である。これは、他の状態遷移図においても同様である。図５に示すように、上位オートマトンには、２つの状態W，Sと、２つの状態遷移(W，S)，(S，W)と、が含まれる。
【００３９】
ステップＳ２において、下位オートマトン記憶部２は、ユーザにより入力された下位オートマトンを記憶する。図６は、下位オートマトンを示す状態遷移図である。図６に示すように、下位オートマトンには、３つの状態G，Y，Rと、３つの状態遷移(G，Y)，(Y，R)，(R，G)と、が含まれる。
【００４０】
なお、上位オートマトン及び下位オートマトンの各状態に付された符号W，S，G，Y，Rは、ユーザにより設定されてもよいし、推定装置により自動的に設定されてもよい。
【００４１】
ステップＳ３において、推定装置は、上位オートマトン記憶部１に記憶された上位オートマトン及び下位オートマトン記憶部２に記憶された下位オートマトンを、表示装置１０３に表示する。表示装置１０３には、図７に示すように、上位オートマトン及び下位オートマトンを示す状態遷移図が表示されてもよいし、状態遷移図のかわりに状態遷移表が表示されてもよい。
【００４２】
ステップＳ４において、対応状態対及び不対応状態対がユーザにより設定される。この設定は、例えば、表示装置１０３に表示された状態遷移図から、対応する、或いは対応しない状態の組を、入力装置１０２によって選択することにより行われる。設定された対応状態対及び不対応状態対は状態対記憶部３に記憶される。
【００４３】
また、推定装置は、設定された対応状態対及び不対応状態対を、表示装置１０３に表示してもよい。図８は、表示装置１０３に表示された対応状態対及び不対応状態対の一例を示す図である。図８において、対応状態対及び不対応状態対は、図７の状態遷移図にオーバーラップして表示されている。破線で接続された状態が対応状態対を示し、一点鎖線で接続された状態が不対応状態対を示す。ここでは、状態Wと状態Gとの組（状態対W−G）が対応状態対として設定され、状態Wと状態Yとの組（状態対W−Y）及び状態Wと状態Rとの組（状態対W−R）が不対応状態対として設定されたものとする。なお、対応状態対及び不対応状態対は、図９に示すように、状態遷移表に表示されてもよい。図９において、対応が○の行が対応状態対を示し、対応が×の行が不対応状態対を示す。
【００４４】
ユーザは、対応状態対及び不対応状態対を設定した後、入力装置１０２によって、設定の終了信号を推定装置に入力する。推定装置は、終了信号を入力されると、論理式の作成を開始する。
【００４５】
ステップＳ５において、論理式作成部４は、まず、対応可能状態対を列挙する。対応可能状態対とは、ステップＳ４において設定された対応状態対及び不対応状態対のいずれにも属さない状態対のことである。ここで、図１０は、対応可能状態対の作成処理を示すフローチャートである。図１０に示すように、対応可能状態対の列挙処理は、以下のように行われる。
【００４６】
ステップＳ５０１において、論理式作成部４は、上位オートマトン及び下位オートマトンに含まれる全ての状態を未選択に設定する。
【００４７】
ステップＳ５０２において、論理式作成部４は、上位オートマトンに未選択の状態があるか判定する。上位オートマトンに未選択の状態がない場合（Ｓ５０２のＮＯ）、処理は終了する。一方、上位オートマトンに未選択の状態がある場合（Ｓ５０２のＹＥＳ）、処理はステップＳ５０３に進む。
【００４８】
ステップＳ５０３において、論理式作成部４は、上位オートマトンの未選択の状態の中から、状態pを１つ選択する。
【００４９】
ステップＳ５０４において、論理式作成部４は、下位オートマトンに未選択の状態があるか判定する。下位オートマトンに未選択の状態がない場合（Ｓ５０４のＮＯ）、処理はステップＳ５０５に進む。
【００５０】
ステップＳ５０５において、論理式作成部４は、下位オートマトンの状態を全て未選択に設定する。その後、処理はステップＳ５０２に戻る。
【００５１】
一方、下位オートマトンに未選択の状態がある場合（Ｓ５０４のＹＥＳ）、処理はステップＳ５０６に進む。
【００５２】
ステップＳ５０６において、論理式作成部４は、下位オートマトンの未選択の状態の中から状態qを１つ選択する。
【００５３】
ステップＳ５０７において、論理式作成部４は、状態対記憶部３を参照して、選択した状態p，qからなる状態対p−qが、対応状態対又は不対応状態対に含まれるか判定する。
【００５４】
状態対p−qが対応状態対及び不対応状態対のいずか一方に含まれる場合（Ｓ５０７のＹＥＳ）、処理はステップＳ５０４に戻る。
【００５５】
一方、状態対p−qが対応状態対及び不対応状態対のいずれにも含まれない場合（Ｓ５０７のＮＯ）、処理はステップＳ５０８に進む。
【００５６】
ステップＳ５０８において、論理式作成部４は、状態対p−qを、対応可能状態対として状態対記億部３に記憶させる。その後、処理はステップＳ５０４に戻る。
【００５７】
以上の処理により、対応可能状態対S−G，S−Y，S−Rが列挙され、状態対記億部３に記憶される。推定装置は、列挙された対応可能状態対を、対応状態対及び不対応状態対とともに、表示装置１０３に表示してもよい。図１１は、表示装置１０３に表示された対応可能状態対、対応状態対、及び不対応状態対の一例を示す図である。図１１において、対応が？の行が対応可能状態対を示す。以下では、対応状態対はW−G、不対応状態対はW−Y，W−R、対応可能状態対はS−G，S−Y，S−Rであるものとする。
【００５８】
ステップＳ６において、論理式作成部４は、論理式を作成する。論理式の作成は、例えば、以下の文献に記載の原理を応用することにより行われる。
Uniform approaches to the verification of finite state systems
Sandeep Kumar Shukla       
Doctoral Dissertation, State University of New York at Albany
【００５９】
ここで、図１２は、論理式の作成処理を示すフローチャートである。図１２に示すように、論理式の作成処理は、以下のように行われる。
【００６０】
ステップＳ６０１において、論理式作成部４は、集合Vを作成する。集合Vとは、状態対記億部３に記憶された各状態対p−qに対応する変数Xp,qの集合である。集合Vは、論理式記憶部５に記憶される。また、状態対p−qと変数Xp,qとの対応関係が状態対記憶部３に記憶される。
【００６１】
ステップＳ６０１の開始時点で、状態対記憶部３には、６つの状態対W−G，W−Y，W−R，S−G，S−Y，S−Rが記憶されているため、論理式作成部４は、各状態対と対応する６つの変数XW,G，XW,Y，XW,R，XS,G，XS,Y，XS,Rを作成する。したがって、V＝｛XW,G，XW,Y，XW,R，XS,G，XS,Y，XS,R｝となる。
【００６２】
ステップＳ６０２において、論理式作成部４は、集合C，Dを作成する。集合C，Dは、論理式の節の集合であり、作成された時点では空集合である。より詳細には、集合Cは、必ずしも真にならなくてもよい節の集合であり、集合Dは、必ず真にならなければならない節の集合である。集合C，Dは、論理式記憶部５に記憶される。
【００６３】
ステップＳ６０３において、論理式作成部４は、集合Vが空集合であるか判定する。Vが空集合である場合（Ｓ６０３のＹＥＳ）、処理はステップＳ６０４に進む。
【００６４】
ステップＳ６０４において、論理式作成部４は、集合C，Dを参照して、論理式を作成する。論理式は、集合Cに含まれる節及び集合Dに含まれる節の論理積となる。作成された論理式は、論理式記憶部５に記憶される。一方、集合Vが空集合でない場合（Ｓ６０３のＮＯ）、処理はステップＳ６０５に進む。
【００６５】
ステップＳ６０５において、論理式作成部４は、集合Vから変数Xp,qを１つ選択する。
【００６６】
ステップＳ６０６において、論理式作成部４は、選択した変数Xp,qを集合Vから除去する（V：＝V−{Xp,q}）。
【００６７】
ステップＳ６０７において、論理式作成部４は、状態対記億部３を参照して、選択した変数Xp,qに対応する状態対p−qが不対応状態対であるか判定する。状態対p−qが不対応状態対である場合（Ｓ６０７のＹＥＳ）、処理はステップＳ６０８に進む。
【００６８】
ステップＳ６０８において、論理式作成部４は、集合Dに節¬Xp,qを追加する（D：＝D∪{¬Xp,q}）。状態対p−qは不対応状態対である場合、節¬Xp,qは必ず真になる。その後、処理はステップＳ６０３に戻る。
【００６９】
一方、状態対p−qが不対応状態対でない場合（Ｓ６０７のＮＯ）、処理はステップＳ６０９に進む。
【００７０】
ステップＳ６０９において、論理式作成部４は、状態対記億部３を参照して、選択した変数Xp,qに対応する状態対p−qが対応状態対であるか判定する。状態対p−qが対応状態対である場合（Ｓ６０９のＹＥＳ）、処理はステップＳ６１０に進む。
【００７１】
ステップＳ６１０において、論理式作成部４は、集合Dに節Xp,qを追加する（D：＝D∪{Xp,q}）。状態対p−qは対応状態対である場合、節Xp,qは必ず真になる。
【００７２】
一方、状態対p−qが対応状態対でない場合（Ｓ６０９のＮＯ）、又はステップＳ６１０の終了後、処理はステップＳ６１１に進む。
【００７３】
ステップＳ６１１において、論理式作成部４は、状態対p−qの状態pに、未選択の状態p′があるか判定する。未選択の状態p′がない場合（ステップＳ６１１のＮＯ）、処理はステップＳ６０３に戻る。一方、未選択の状態p′がある場合（ステップＳ６１１のＹＥＳ）、処理はステップＳ６１２に進む。
【００７４】
ステップＳ６１２において、論理式作成部４は、未選択の状態p′の中から、状態p′を１つ選択する。
【００７５】
ステップ６１３において、集合Eを作成する。集合Eは、変数Xp,qに対応する変数Xp′,q′の論理和（∨Xp′,q′）と同様の意味を持ち、作成された時点では空集合である。集合Eは、論理式記憶部５に記憶される。
【００７６】
ステップＳ６１４において、論理式作成部４は、状態対p−qの状態qに、未選択の状態q′があるか判定する。未選択の状態q′がない場合（ステップＳ６１４のＮＯ）、処理はステップＳ６１５に進む。
【００７７】
ステップＳ６１５において、論理式作成部４は、集合Cに節¬Xp,q∨（∨E）を追加する（C：＝C∪{¬Xp,q∨（∨E）}）。ただし、（∨E）はEに含まれる論理式すべての論理和を表す。節¬Xp,q∨（∨E）は、下位オートマトンが上位オートマトンを模倣する場合に真となり、下位オートマトンが上位オートマトンを模倣しない場合に偽となる。このため、¬Xp,q∨（∨E）は、必ずしも真になるとは限らない節である。その後、処理はステップＳ６１１に戻る。一方、未選択の状態q′がある場合（ステップＳ６１４のＹＥＳ）、処理はステップＳ６１６に進む。
【００７８】
ステップＳ６１６において、論理式作成部４は、未選択の状態q′の中から、状態q′を１つ選択する。
【００７９】
ステップＳ６１７において、論理式作成部４は、状態対記憶部３を参照して、集合Eに、Xp′,q′を追加する（E：＝E∪Xp′,q′）。その後、処理はステップＳ６１４に戻る。
【００８０】
ここで、ステップＳ６０３〜ステップＳ６１７について、より詳細に説明する。以下では、ステップＳ６０１において、XW,G，XW,Y，XW,R，XS,G，XS,Y，XS,Rからなる集合Vが作成され、ステップＳ６０５において、この順番で変数が選択されるものとする。
【００８１】
まず、V＝｛XW,G，XW,Y，XW,R，XS,G，XS,Y，XS,R｝であるから（Ｓ６０３のＮＯ）、論理式作成部４は、変数XW,Gを選択し（Ｓ６０５）、集合Vから変数XW,Gを除去する（Ｓ６０６）。これにより、V＝｛XW,Y，XW,R，XS,G，XS,Y，XS,R｝となる。状態対W−Gは対応状態対であるから（Ｓ６０９のＹＥＳ）、論理式作成部４は、集合DにXW,Gを追加する（Ｓ６１０）。
【００８２】
状態Wには未選択の後続状態Sがあるから（Ｓ６１１のＹＥＳ）、論理式作成部４は、状態Sを選択し（Ｓ６１２）、集合E＝φを作成する（Ｓ６１３）。また、状態Gには未選択の後続状態Yがあるから（Ｓ６１４のＹＥＳ）、論理式作成部４は、状態Yを選択し（Ｓ６１６）、集合EにXS,Yを追加する（E:=E∪XS,Y）（Ｓ６１７）。状態Gには状態Yの他に後続状態がないから（Ｓ６１４のＮＯ）、論理式作成部４は、集合Cに¬XW,G∨XS,Yを追加する（Ｓ６１５）。状態Wには状態Sの他に後続状態がないから（Ｓ６１１のＮＯ）、処理はステップＳ６０３に戻り、XW,Gに関する処理が終了する。
【００８３】
次に、V＝｛XW,Y，XW,R，XS,G，XS,Y，XS,R｝であるから（Ｓ６０３のＮＯ）、論理式作成部４は、変数XW,Yを選択し（Ｓ６０５）、集合Vから変数XW,Yを除去する（Ｓ６０６）。これにより、V＝｛XW,R，XS,G，XS,Y，XS,R｝となる。状態対W−Yは不対応状態対であるから（Ｓ６０７のＹＥＳ）、論理式作成部４は、集合Dに¬XW,Yを追加する（Ｓ６０８）。その後、処理はステップＳ６０３に戻り、XW,Yに関する処理が終了する。
【００８４】
次に、V＝｛XW,R，XS,G，XS,Y，XS,R｝であるから（Ｓ６０３のＮＯ）、論理式作成部４は、変数XW,Rを選択し（Ｓ６０５）、集合Vから変数XW,Rを除去する（Ｓ６０６）。これにより、V＝｛XS,G，XS,Y，XS,R｝となる。状態対W−Rは不対応状態対であるから（Ｓ６０７のＹＥＳ）、論理式作成部４は、集合Dに¬XW,Rを追加する（Ｓ６０８）。その後、処理はステップＳ６０３に戻り、XW,Rに関する処理が終了する。
【００８５】
次に、V＝｛XS,G，XS,Y，XS,R｝であるから（Ｓ６０３のＮＯ）、論理式作成部４は、変数XS,Gを選択し（Ｓ６０５）、集合Vから変数XS,Gを除去する（Ｓ６０６）。これにより、V＝｛XS,Y，XS,R｝となる。状態対S−Gは対応可能状態対であるから（Ｓ６０９のＮＯ）、処理はステップＳ６１１に進む。
【００８６】
状態Sには未選択の後続状態Wがあるから（Ｓ６１１のＹＥＳ）、論理式作成部４は、状態Wを選択し（Ｓ６１２）、集合E＝φを作成する（Ｓ６１３）。また、状態Gには未選択の後続状態Yがあるから（Ｓ６１４のＹＥＳ）、論理式作成部４は、状態Yを選択し（Ｓ６１６）、集合EにXW,Yを追加する（E:=E∪XW,Y）（Ｓ６１７）。状態Gには状態Yの他に後続状態がないから（Ｓ６１４のＮＯ）、論理式作成部４は、集合Cに¬XS,G∨XW,Yを追加する（Ｓ６１５）。状態Sには状態Wの他に後続状態がないから（Ｓ６１１のＮＯ）、処理はステップＳ６０３に戻り、XS,Gに関する処理が終了する。
【００８７】
次に、V＝｛XS,Y，XS,R｝であるから（Ｓ６０３のＮＯ）、論理式作成部４は、変数XS,Yを選択し（Ｓ６０５）、集合Vから変数XS,Yを除去する（Ｓ６０６）。これにより、V＝｛XS,R｝となる。状態対S−Yは対応可能状態対であるから（Ｓ６０９のＮＯ）、処理はステップＳ６１１に進む。
【００８８】
状態Sには未選択の後続状態Wがあるから（Ｓ６１１のＹＥＳ）、論理式作成部４は、状態Wを選択し（Ｓ６１２）、集合E＝φを作成する（Ｓ６１３）。また、状態Yには未選択の後続状態Rがあるから（Ｓ６１４のＹＥＳ）、論理式作成部４は、状態Rを選択し（Ｓ６１６）、集合EにXW,Rを追加する（E:=E∨XW,R）（Ｓ６１７）。状態Yには状態Rの他に後続状態がないから（Ｓ６１４のＮＯ）、論理式作成部４は、集合Cに¬XS,Y∨XW,Rを追加する（Ｓ６１５）。状態Sには状態Wの他に後続状態がないから（Ｓ６１１のＮＯ）、処理はステップＳ６０３に戻り、XS,Yに関する処理が終了する。
【００８９】
次に、V＝｛XS,R｝であるから（Ｓ６０３のＮＯ）、論理式作成部４は、変数XS,Rを選択し（Ｓ６０５）、集合Vから変数XS,Rを除去する（Ｓ６０６）。これにより、V＝φとなる。状態対S−Rは対応可能状態対であるから（Ｓ６０９のＮＯ）、処理はステップＳ６１１に進む。
【００９０】
状態Sには未選択の後続状態Wがあるから（Ｓ６１１のＹＥＳ）、論理式作成部４は、状態Wを選択し（Ｓ６１２）、集合E＝φを作成する（Ｓ６１３）。また、状態Rには未選択の後続状態Gがあるから（Ｓ６１４のＹＥＳ）、論理式作成部４は、状態Gを選択し（Ｓ６１６）、集合EにXW,Gを追加する（E:=E∪XW,G）（Ｓ６１７）。状態Rには状態Gの他に後続状態がないから（Ｓ６１４のＮＯ）、論理式作成部４は、集合Cに¬XS,Y∨XW,Gを追加する（Ｓ６１５）。状態Sには状態Wの他に後続状態がないから（Ｓ６１１のＮＯ）、処理はステップＳ６０３に戻り、XS,Rに関する処理が終了する。
【００９１】
その後、V＝φであるから（Ｓ６０３のＹＥＳ）、論理式作成部４は、以上の処理により作成された集合C，Dに基づいて、論理式を作成する（Ｓ６０４）。
【００９２】
図１３は、以上の処理により論理式記憶部５に記憶された集合C，Dを示す図である。図１３に示すように、集合Cには、¬XW,G∨XS,Y，¬XS,G∨XW,Y，¬XS,Y∨XW,R，¬XS,R∨XW,Gが含まれる。集合Dには、XW,G，¬XW,Y，¬XW,Rが含まれる。
【００９３】
論理式作成部４は、図１３の集合C，Dに基づいて論理式を作成する（Ｓ６０４）。論理式は、集合C，Dに含まれる節の論理積であるから、以下の論理式が作成される。
（¬XW,G∨XS,Y）∧（¬XS,G∨XW,Y）∧（¬XS,Y∨XW,R）∧（¬XS,R∨XW,G）∧（XW,G）∧（¬XW,Y）∧（¬XW,R）
作成された論理式は、論理式記憶部５に記憶される。
【００９４】
なお、対応状態対及び不対応状態対が設定されていない場合には、上記のステップＳ６０２及びステップＳ６０７〜Ｓ６１０は省略することができる。この場合、集合Dは不要となる。
【００９５】
ステップＳ７において、論理式求解部６は、論理式記憶部５に記憶された論理式の解を求める。この際、論理式求解部６は、集合Dに含まれる節が真となり、かつ、集合Cに含まれる節のうち真となる節が最大となるように解を求める。すなわち、集合Dに含まれる節はPartial Max-Sat問題におけるハード節となり、集合Cに含まれる節はソフト節となる。上記の論理式に対して得られた解は、｛XW,G=1，XW,Y=0，XW,R=0，XS,G=0，XS,Y=1，XS,R=1｝であるものとする。得られた解は、解記憶部７に記憶される。
【００９６】
ステップＳ８において、対応関係抽出部８は、論理式記憶部５に記憶された論理式と、解記憶部７に記憶された解と、状態対記憶部３に記憶された状態対と変数との対応関係とに基づいて、上位オートマトンと下位オートマトンとの対応関係を抽出する。
【００９７】
ここで、図１４は、対応関係の抽出処理を示すフローチャートである。図１４に示すように、対応関係の抽出処理は、以下のように行われる。
【００９８】
まず、状態間の対応関係の抽出処理について説明する。
【００９９】
ステップＳ８０１において、対応関係抽出部８は、解記憶部７に記憶された解を参照して、解の中から真である変数Xp,qを選択する。これにより、変数XW,G，XS,Y，XS,Rが選択される。
【０１００】
ステップＳ８０２において、対応関係抽出部８は、状態対記憶部３に記憶された状態対と変数との対応関係を参照して、選択した変数と対応する状態対を抽出する。これにより、状態対W−G，S−Y，S−Rが抽出される。
【０１０１】
ステップＳ８０３において、対応関係記憶部９は、抽出された状態対を推定対応状態対として記憶する。推定対応状態対とは、上位オートマトンと下位オートマトンとの対応関係の一致の尤度が最大となるように両者の対応関係を推定した場合に対応する状態対である。したがって、推定対応状態対は必ずしも対応状態対であるとは限らない。
【０１０２】
これにより、対応関係記憶部９には、推定対応状態対W−G，S−Y，S−Rが記憶され、状態間の対応関係の抽出が終了する。
【０１０３】
なお、対応関係抽出部８は、解の中から偽である変数Xp,qを選択し、上記と同様の処理によって、推定不対応状態対を抽出してもよい。推定不対応状態対とは、上位オートマトンと下位オートマトンとの対応関係の一致の尤度が最大となるように両者の対応関係を推定した場合に対応しない状態対である。したがって、推定不対応状態対は必ずしも不対応状態対であるとは限らない。
【０１０４】
次に、状態遷移間の対応関係の抽出処理について説明する。
【０１０５】
ステップＳ８０４において、対応関係抽出部８は、論理式記憶部５に記憶された論理式に、解記憶部７に記憶された解を代入して、偽となる節を選択する。論理式求解部６は、集合Dに含まれる節が真になるように解を求めるため、ここで選択される節は集合Cに含まれる節¬Xp,q∨Xp′,q′となる。
【０１０６】
集合Cには、４つの節¬XW,G∨XS,Y，¬XS,G∨XW,Y，¬XS,Y∨XW,R，¬XS,R∨XW,Gが含まれる。このうち解を代入して偽となる節は、¬XS,Y∨XW,Rだけである。したがって、対応関係抽出部８は、節¬XS,Y∨XW,Rを選択する。
【０１０７】
ステップＳ８０５において、対応関係抽出部８は、選択した節¬Xp,q∨Xp′,q′から、状態遷移（q，q′）を抽出する。ここでは、節¬XS,Y∨XW,Rから、状態遷移（Y，R）が抽出される。
【０１０８】
ステップＳ８０６において、対応関係記憶部９は、抽出された状態遷移を推定不対応状態遷移として記憶する。推定不対応状態遷移とは、上位オートマトンと下位オートマトンとの対応関係の一致の尤度が最大となるように両者の対応関係を推定した場合に対応しない状態遷移である。したがって、推定不対応状態遷移は必ずしも対応しない状態遷移であるとは限らない。
【０１０９】
これにより、対応関係記憶部９には、推定不対応状態遷移（Y，R）が記憶され、状態遷移間の対応関係の抽出が終了する。
【０１１０】
なお、対応関係抽出部８は、選択した節¬Xp,q∨Xp′,q′から、状態遷移（p，p′）を推定不対応状態遷移として抽出してもよい。
【０１１１】
また、対応関係抽出部８は、真となる節を選択し、上記と同様の処理によって、推定対応状態遷移を抽出してもよい。推定対応状態遷移とは、上位オートマトンと下位オートマトンとの対応関係の一致の尤度が最大となるように両者の対応関係を推定した場合に対応する状態遷移である。したがって、推定対応状態遷移は必ずしも対応しない状態遷移であるとは限らない。
【０１１２】
さらに、対応関係抽出部８は、状態遷移間の対応関係を抽出した後に、状態間の対応関係を抽出してもよい。
【０１１３】
ステップＳ９において、推定装置は、対応関係記憶部９に記憶した上位オートマトンと下位オートマトンとの対応関係を表示装置１０３に表示する。
【０１１４】
図１５は、表示装置１０３に表示された状態間の対応関係の一例を示す図である。図１５において、対応が○の行が対応状態対を示し、対応が×の行が不対応状態対を示し、対応が！の行が推定対応状態対を示す。状態対W−Gは、推定対応状態対として対応関係記憶部９に記憶されているが、予め対応状態対に設定されているため、図１５では対応状態対として表示されている。
【０１１５】
図１６は、表示装置１０３に表示された状態間の対応関係の他の例を示す図である。図１６において、状態間の対応関係は、状態遷移図にオーバーラップして表示されている。破線で接続された状態が対応状態対を示し、一点鎖線で接続された状態が不対応状態対を示し、点線で接続された状態が推定対応状態対を示す。
【０１１６】
図１７は、表示装置１０３に表示された状態遷移間の対応関係の一例を示す図である。図１７において、推定不対応状態遷移（Y，R）は、不一致遷移Y→Rという形式で表示されている。
【０１１７】
なお、表示装置１０３に表示される上位オートマトンと下位オートマトンとの対応関係は、図１５〜図１７に限られない。
【０１１８】
以上説明した通り、本実施形態に係る推定装置によれば、上位オートマトンと下位オートマトンとの対応関係を、一致の尤度が高くなるように推定することができる。これにより、仕様書から生成されたオートマトンとソースコードから生成されたオートマトンとのように、抽象度や記述者の違いにより、対応を推定することが困難な２つのオートマトン間の対応関係を機械的に推定することができる。
【０１１９】
また、状態間や状態遷移間の対応関係を抽出することにより、仕様書の不備や、ソースコードの不具合の推定が可能となる。
【０１２０】
なお、本発明は上記各実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記各実施形態に開示されている複数の構成要素を適宜組み合わせることによって種々の発明を形成できる。また例えば、各実施形態に示される全構成要素からいくつかの構成要素を削除した構成も考えられる。さらに、異なる実施形態に記載した構成要素を適宜組み合わせてもよい。
【符号の説明】
【０１２１】
１：上位オートマトン記憶部、２：下位オートマトン記憶部、３：状態対記億部、４：論理式作成部、５：論理式記憶部、６：論理式求解部、７：解記憶部、８：対応関係抽出部、９：対応関係記憶部、１０：下位オートマトン生成部、１００：コンピュータ装置、１０１：ＣＰＵ、１０２：入力装置、１０３：表示装置、１０４：通信装置、１０５：主記憶装置、１０６：外部記憶装置、１０７：ハブ
【図１】
2016057978.tif 000003
【図２】
2016057978.tif 000004
【図３】
2016057978.tif 000005
【図４】
2016057978.tif 000006
【図５】
2016057978.tif 000007
【図６】
2016057978.tif 000008
【図７】
2016057978.tif 000009
【図８】
2016057978.tif 000010
【図９】
2016057978.tif 000011
【図１０】
2016057978.tif 000012
【図１１】
2016057978.tif 000013
【図１２】
2016057978.tif 000014
【図１３】
2016057978.tif 000015
【図１４】
2016057978.tif 000016
【図１５】
2016057978.tif 000017
【図１６】
2016057978.tif 000018
【図１７】
2016057978.tif 000019