(57)【要約】【課題】状態遷移図や状態遷移表を作成することなく、これまでの設計の最終成果である手続き型言語で書かれたソースコードから状態遷移モデルを生成する。【解決手段】補完変数抽出部は、ソースコードと、状態変数を指定する情報である状態変数指定情報と、状態分割ポイントとなる手続きを指定する情報である状態分割ポイント指定情報から、各状態分割ポイント間で、状態変数の値を計算する際必要となる変数である補完変数を抽出する。状態遷移モデル生成部は、状態変数および補完変数に関する手続きに基づいて、状態分割ポイントでの各状態変数、補完変数の値を定め、状態分割ポイントと、状態変数の値と、補完変数の値とで記述されたノードと、状態がその遷移先の状態へ遷移することを示すエッジであって、遷移のきっかけとなるイベントと、その条件が真のときにだけ遷移が許される条件とを含むエッジとを用いて記述される状態遷移モデルのデータを生成する。【選択図】図４
2015069617.tif 000002
【特許請求の範囲】
【請求項１】
状態遷移モデルを生成する対象であって、手続き型言語で記述された命令文の集合であるソースコードと、ソースコードに含まれる状態変数を指定する情報である状態変数指定情報と、ソースコードに含まれる状態分割ポイントとなる手続きを指定する情報である状態分割ポイント指定情報から、各状態分割ポイント間で、状態変数の値を計算する際必要となる変数である補完変数を抽出する抽出手段と、
ソースコード中の状態変数および補完変数に関する手続きに基づいて、状態分割ポイントでの各状態変数、補完変数の値を定め、
状態分割ポイントと、状態変数の値と、補完変数の値とで記述されたノードと、
状態がその遷移先の状態へ遷移することを示すエッジであって、前記遷移のきっかけとなるイベントと、その条件が真のときにだけ遷移が許される条件とを含むエッジと
を用いて記述される状態遷移モデルデータを生成する生成手段と、
を有する状態遷移モデル生成装置。
【請求項２】
前記ノードに補完変数の値が含まれている場合、前記ノードから補完変数の値を削除し、当該補完変数の値を当該ノードのエッジにおける条件として書き換える再構成手段をさらに有する、請求項１に記載の状態遷移モデル生成装置。
【請求項３】
状態遷移モデルを生成する対象であって、手続き型言語で記述された命令文の集合であるソースコードと、ソースコードに含まれる状態変数を指定する情報である状態変数指定情報と、ソースコードに含まれる状態分割ポイントとなる手続きを指定する情報である状態分割ポイント指定情報から、各状態分割ポイント間で、状態変数の値を計算する際必要となる変数である補完変数を抽出する抽出手段と、
ソースコードを解析して、各状態分割ポイントでの補完変数の値域を計算する計算手段と、
ソースコードにおける補完変数の値の書き換えポイントで、補完変数を具体的な値ごとの手続きに書き換える書き換え手段と、
前記書き換え手段によって書き換えられたソースコード中の状態変数に関する手続きに基づいて、状態分割ポイントでの各状態変数の値を定め、
状態分割ポイントと、状態変数の値とを用いて記述されたノードと、
状態がその遷移先の状態へ遷移することを示すエッジであって、前記遷移のきっかけとなるイベントと、その条件が真のときにだけ遷移が許される条件とを含むエッジと
を用いて記述される状態遷移モデルのデータを生成する生成手段と
を有する状態遷移モデル生成装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本明細書に記載の実施の形態は、状態遷移モデル生成装置に関する。
【背景技術】
【０００２】
ソフトウェア開発、特に組込みシステムでは、誤りや漏れのない仕様を記述するために状態遷移図や状態遷移表を用いて設計をする。この時に誤りや漏れの無い状態遷移を効率的に記述する方法が望まれている。従来の状態遷移設計では、状態遷移モデルで設計を行い、詳細化し、コードを生成していた。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開平６−２１５０６６号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
状態遷移設計は、これまでの設計方法とは根本的に異なるため、これまでの設計資産を流用し難い。また、状態遷移設計されていないものから、状態遷移モデルによる設計に移行、改良は困難であるという問題があった。
【０００５】
本発明の目的は、状態遷移設計を行うために、状態遷移図や状態遷移表を作成することなく、これまでの設計の最終成果である手続き型言語で書かれたソースコード（プログラム）から状態遷移モデルを生成する技術を提供することにある。
【課題を解決するための手段】
【０００６】
本発明の実施の形態は状態遷移モデル生成装置として提案される。状態遷移モデル生成装置は、抽出手段と、生成手段とを有する。
【０００７】
抽出手段は、状態遷移モデルを生成する対象であって、手続き型言語で記述された命令文の集合であるソースコードと、ソースコードに含まれる状態変数を指定する情報である状態変数指定情報と、ソースコードに含まれる状態分割ポイントとなる手続きを指定する情報である状態分割ポイント指定情報から、各状態分割ポイント間で、状態変数の値を計算する際必要となる変数である補完変数を抽出する。
【０００８】
生成手段は、ソースコード中の状態変数および補完変数に関する手続きに基づいて、状態分割ポイントでの各状態変数、補完変数の値を定め、状態分割ポイントと、状態変数の値と、補完変数の値とで記述されたノードと、状態がその遷移先の状態へ遷移することを示すエッジであって、前記遷移のきっかけとなるイベントと、その条件が真のときにだけ遷移が許される条件とを含むエッジとを用いて記述される状態遷移モデルのデータを生成する。
【０００９】
状態遷移モデル生成装置は、前記ノードに補完変数の値が含まれている場合、前記ノードから補完変数の値を削除し、当該補完変数の値を当該ノードのエッジにおける条件として書き換える再構成手段をさらに有していてもよい。
【図面の簡単な説明】
【００１０】
【図１】UMLの状態遷移モデル（ステートチャート図）の例を示す図
【図２】独立関連である例のソースコードを示す図
【図３】独立関連でない例のソースコードを示す図
【図４】状態遷移モデル生成装置の構成例を示す機能ブロック図
【図５】状態遷移モデル生成装置１に入力されるソースコードの一部を示す図
【図６】状態分割ポイントの並びを説明するための、ソースコードの例を示す図
【図７】補完変数の例を説明するためのソースコードを示す図
【図８】状態遷移モデル生成装置１の主たる動作である状態遷移モデル生成処理のフローチャート
【図９Ａ】補完変数抽出処理の例を示すフローチャート
【図９Ｂ】図９Ａに続くフローチャート
【図１０】網羅状態遷移モデル生成処理の例を示すフローチャート
【図１１Ａ】状態遷移モデル再構成処理の例を示すフローチャート
【図１１Ｂ】図１１Ａに続くフローチャート
【図１２Ａ】状態遷移モデルを生成させるソースコードを示す図
【図１２Ｂ】図１２Ａに続くソースコードを示す図
【図１２Ｃ】図１２Ｂに続くソースコードを示す図
【図１２Ｄ】図１２Ｃに続くソースコードを示す図
【図１３Ａ】図１２Ａから図１２Ｄに示したソースコードから状態遷移モデル生成部３００が生成した網羅状態遷移モデルのデータ例を示す図
【図１３Ｂ】図１３Ａに続く網羅状態遷移モデルのデータ例を示す図
【図１３Ｃ】図１３Ｂに続く網羅状態遷移モデルのデータ例を示す図
【図１４】図１３Ａ、図１３Ｂ、図１３Ｃに示す網羅状態遷移モデルのデータから生成されるステートチャートの例を示す図
【図１５Ａ】図１３Ａから図１３Ｃに示した網羅状態遷移モデルのデータから生成した補完変数を含まない状態遷移モデルのデータ例を示す図
【図１５Ｂ】図１５Ａに続く状態遷移モデルのデータ例を示す図
【図１６】図１３Ａ、図１３Ｂ、図１３Ｃに示す網羅状態遷移モデルのデータから生成されるステートチャートの例を示す図
【図１７】本実施の形態に係る状態遷移モデル生成装置の構成例を示す機能ブロック図
【図１８Ａ】第２の実施の形態に係る状態遷移モデル生成装置で状態遷移モデルを生成させるソースコードの例を示す図
【図１８Ｂ】図１８Ａに続くソースコードの例を示す図
【図１８Ｃ】図１８Ｂに続くソースコードの例を示す図
【図１８Ｄ】図１８Ｃに続くソースコードの例を示す図
【図１８Ｅ】図１８Ｄに続くソースコードの例を示す図
【図１９Ａ】補完変数離散値パス分解部によって書き換えられたソースコードの例を示す図
【図１９Ｂ】図１９Ａに続くソースコードの例を示す図
【図１９Ｃ】図１９Ｂに続くソースコードの例を示す図
【図１９Ｄ】図１９Ｃに続くソースコードの例を示す図
【図２０Ａ】状態遷移モデル生成部によって生成される状態遷移モデルのデータ５００の例を示す図
【図２０Ｂ】図２０Ａに続くデータの例を示す図
【図２１】図２０Ａ、図２０Ｂに示した状態遷移モデルのデータ図から生成されるステートチャートの例を示す
【図２２】第２の実施の形態にかかる状態遷移モデル生成装置の主たる動作である状態遷移モデル生成処理のフローチャート
【発明を実施するための形態】
【００１１】
以下、図面を参照して本発明の実施の形態に係る通信システムを説明する。
[０．用語の定義]
本明細書中で使用する用語の定義を述べる。
[０．１．手続き型言語]
「手続き型言語」とは、「手続き呼び出し」の概念に基づくプログラミングパラダイムの元に作られた言語をいう。「手続き」はプロシージャ、ルーチン、サブルーチン、メソッド、関数（数学の関数とは異なる。）など様々な呼称があるが、実行すべき一連の計算ステップを持つものをいう。「手続き」はプログラム実行中の任意の時点で呼び出すことができ、他の手続きからの呼び出しも、自分自身からの呼び出し（再帰呼び出し）も含まれる。
一連の計算ステップでは、記述された命令を逐次的に実行し、処理の結果に応じて変数の内容を変化させていく。
ほとんど全ての手続き型言語では以下を記述可能である。
（１）変数
（２）変数の値の読み取り
（３）変数の値の書き換え
（４）変数の値に関する条件判定と手続きの分岐（ジャンプを含む）
【００１２】
[０．２．C言語]
「C言語」とは、手続き型言語の１つである。産業界で広く使われている。C言語（Cげんご）は、1972年にAT&Tベル研究所のデニス・リッチーが主体となって作ったプログラミング言語である。英語圏では単にCと呼称されており、日本でも文書や文脈によっては同様に C と呼称される。C言語にはいくつかの規格があるが、ここでは、C89を指す。ISOとANSIは協同で C 言語の規格の標準化を進め、1989年12月にANSIがANSI X3.159-1989, American National Standard for Information Systems -Programming Language-Cを、1990年12月に ISO がINTERNATIONAL STANDARD ISO/IEC 9899: 1990(E) Programming Languages-Cを発行した。ISO 規格のほうが章立てが追加されており、その後ANSIも ISO 規格にならって章立てを追加した。それぞれ C89（ANSI C89）及び ISO C90 という通称で呼ばれることがある。日本では、これを翻訳したものが日本工業規格『JIS X3010-1993 プログラム言語C』として、1993年10月に制定された。
【００１３】
[０．３．UMLの状態遷移モデル（ステートチャート図）]
「UMLの状態遷移モデル（ステートチャート図）」は、ＵＭＬ（Unified Modeling Language）の定めるダイアグラムの一つであって、簡略記述が可能なように拡張されたものをいう。UMLの状態遷移モデルでは、エッジに状態の入口と出口にアクションが記述可能である。例えば、ある状態に入る全てのエッジに共通のアクションがある場合、 エッジに同一のアクションを記述するかわりに、 entry/ アクション として記述できる。図１に、UMLの状態遷移モデル（ステートチャート図）の例を示す。
【００１４】
また、継続的に行う動作は、 do/ アクティビティ として記述する。また、階層表現や、並列表現もサポートする。また変数の記述も可能である。本明細書ではアクションや、条件はC言語の形式（制約あり）で記述することとする。
本明細書中で、「状態遷移モデル」という場合、UMLの状態遷移モデルを指すものとする。
【００１５】
[０．４．構文ポイント、ポイント]
「構文ポイント」とは、プログラム（ソースコード）において各命令のプログラム上の位置をいう。なお、文脈上わかる場合には単にポイントということがある。
【００１６】
[０．５．実行パス]
「実行パス」とは、プログラムの実行を表すもので、実行順序順に並んだ構文ポイントの列を実行パスという。構文ポイントA、Bに対し、あるパスが構文ポイントAで始まり構文ポイントBで終わっている時、このパスをAからBへの実行パスと言う。全実行パスの集合は無限集合となる場合がある。
【００１７】
[０．６．状態分割ポイント]
「状態分割ポイント」とは、状態を分割するプログラム（ソースコード）での構文ポイントの位置を状態分割ポイントという。通常、状態分割ポイントとして、イベント待ちに対応するAPI群を指定するが、これに限定されるものではない。デフォルトでプログラムtskポイントを含む。
【００１８】
[０．７．状態変数]
「状態変数」とは、状態を張る変数として与えられる変数をいう。状態遷移モデルの状態空間Tは、状態分割ポイントの集合をG、状態変数をx1, x2, ..., xnとし、各変数の値域の集合をX1, X2, ..., Xnとすると、T={(g,(a1,a2,...,an))|g∈G. ai∈Xi} で表される。生成される状態遷移モデルの状態の集合はTの部分集合となる。
【００１９】
[０．８．状態変数書換えポイント]
「状態変数書換えポイント」とは、状態変数の値を変更する構文ポイントをいう。
【００２０】
[０．９．連結]
状態分割ポイントAから状態分割ポイントBへの実行パスが存在するとき、状態分割ポイントAは状態分割ポイントBと「連結」であるという。
【００２１】
[０．１０．独立]
状態分割ポイントA、Bが連結であり、変数xのスコープが状態分割ポイントA、Bを含むとする。状態分割ポイントAからBへのすべての実行パスで変数xの状態分割ポイントBでの値が、変数xの状態分割ポイントAでの値に依存しないとき、変数ｘは状態分割ポイントA、B間で「独立」であるという。
【００２２】
[０．１１．後続状態分割ポイント、後続連結、後続連結パス]
状態分割ポイントA、Bが連結であるとする。状態分割ポイントAから状態分割ポイントBへのある実行パスαで、状態分割ポイントBが最初に現れる状態分割ポイントであるとき、状態分割ポイントBは状態分割ポイントAの「後続状態分割ポイント」とである、または単に状態分割ポイントAは状態分割ポイントBと「後続連結」であるという。また、このような実行パスαを状態分割ポイントAから状態分割ポイントBの後続連結パスという。
【００２３】
[０．１２．支配状態分割ポイント、被支配状態変数書換えポイント、被支配パス]
状態分割ポイントAは状態分割ポイントBと後続連結であるとする。状態書換えポイントpがある状態分割ポイントAから状態分割ポイントBの後続連結パスαに含まれるとき、状態書換えポイントpは状態分割ポイントAの「被支配状態変数書換えポイント」という。このとき実行パスαを状態書換えポイントpの状態分割ポイントAに対する「被支配パス」という。また、状態書換えポイントpがAの被支配状態変数書換えポイントであるとき、状態分割ポイントAは状態書換えポイントpの「支配状態分割ポイント」という。
【００２４】
[０．１３．書換えパス集合、完全書換えパス集合]
状態分割ポイントAは状態分割ポイントBと後続連結であるとする。状態分割ポイントAから状態分割ポイントBの全後続連結パスの集合において、状態分割ポイントAでの状態変数の値に関わらず状態分割ポイントBでの状態変数の値が等しくなる後続連結パスのいくつかを１つにまとめることで作られる集合を、状態分割ポイントAから状態分割ポイントBへの「書換えパス集合」という。また、この集合の元を状態分割ポイントAから状態分割ポイントBへの「書換えパス」という。特に、集合からどの二つの書換えパスをとっても、状態分割ポイントAでの状態変数の値に関わらず状態分割ポイントBでの状態変数の値が等しくなるものがないならば、この集合を、状態分割ポイントAから状態分割ポイントBへの「完全書換えパス集合」と呼ぶ。
【００２５】
また、Atsk の全後続連結パスの集合で、状態分割ポイントAでの状態変数の値が(a1, a2, ..., an)であるとき、状態分割ポイントBでの状態変数の値が等しくなる実行パスのいくつかを１つにまとめることで作られる集合を、(a1, a2, ..., an)に対する状態分割ポイントAから状態分割ポイントBへの「書換tsk集合」という。また、この集合の元を(a1, a2, ..., an)に対する状態分割ポイントAから状態分割ポイントBへの「書換えパス」という。特に、集合からどの二つの書換えパスをとっても、状態分割ポイントAでの状態変数の値が(a1, a2, ..., an)であるとき、状態分割ポイントBでの状態変数の値が等しくなるものがないならば、この集合を、(a1, a2, ..., an)に対する状態分割ポイントAから状態分割ポイントBへの「完全書換え実行パス集合」と呼ぶ。
【００２６】
全後続連結パスの集合が無限集合の場合でも、書換えパス集合は有限となる場合がある。書換えパス集合が無限になる場合でも、状態変数の値(a1, a2, ..., an)に対する書換えパス集合は有限になる場合がある（しかし無限になる場合も残る）。
【００２７】
[０．１４．拡大写像、真拡大写像、補完変数]
状態変数をx1, x2, ..., xn、Gを状態分割ポイントの集合とする。ｆ(A∈G) ∈{x|xは状態分割ポイントAをスコープに含む、状態変数以外の変数の部分集合としたとき、B∈G、Bが後続分割ポイントとなるA∈G、状態分割ポイントAから状態分割ポイントBへの書換えパスpとしたとき、A, B, pの定め方によらず、Aでの状態変数の値とf(A)の変数の値から、Bの状態変数の値とf(B)の変数の値を定めることができるならばfは「拡大写像」であるという。またfが拡大写像であるとき、f(A)をfにおけるAの補完tskぶ。またfが拡大写像であるとしたとき、
∀A∈G.(g(A)⊆f(A))
を満たす全てのgでgが拡大写像となるものがfのみならば、fは「真拡大写像」であるという。
【００２８】
[０．１５．独立関連]
状態変数書換えポイントpが状態分割ポイントAの被支配状態変数書換えポイントとする。状態変数書換えポイントpにおいて、参照式中に現れる変数xが、ある状態分割ポイントAに対する被支配パスで、状態分割ポイントAでの状態変数の値と定数で表せないとき、変数xは状態変数書換えポイントpで状態分割ポイントAと独立関連という。
以下に、独立関連の例を示す。状態変数をa1、a2とする。
【００２９】
図２に変数ｘは状態変数書換えポイントpで状態分割ポイントAと独立関連である例のソースコードを示す。また、図３に変数xは状態変数書換えポイントpで状態分割ポイントAと独立関連でない例のソースコードを示す。変数xはa1+1で置き換えられる、すなわち状態変数書き換えポイントpで変数xは状態分割ポイントAでの状態変数の値と定数で表せる、すなわち独立関連ではない。
【００３０】
[０．１６．支配変数、完全支配変数]
変数xは状態変数書換えポイントpで状態分割ポイントAと独立関連であるとする。状態分割ポイントAに対するすべての被支配パスで、スコープ内に状態分割ポイントAが入ってる変数 y1, y2, …, ynと定数の状態分割ポイントAでの値により、状態変数書換えポイントpでの変数xの値が表せるとき、変数y1, y2, …, ynを変数xの支配変数という。さらに、変数yiの値が欠けても、ある状態分割ポイントAに対する被支配パスで変数pの値が表現できなくなる時、変数y1, y2, …, ynは変数xの完全支配変数であると言う。なお、支配変数が存在しない場合もある。
【００３１】
[１．第１の実施の形態]
本発明の第１の実施の形態は、状態遷移モデル生成装置として提案される。この状態遷移モデル生成装置は、手続き型言語によって記述されたソースコードに含まれる、状態を表す変数（状態変数）を用いて状態遷移モデルを生成する装置である。
【００３２】
状態遷移モデル生成装置は、情報処理装置であって、この情報処理装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読み出し専用メモリ（ROM）、入出力装置（Ｉ／Ｏ）、及び必要な場合にはハードディスク装置等の外部記憶装置を具備している装置である。
ユーザは、ソースコード中の変数であって状態変数であるものを状態変数指定情報として状態遷移モデル生成装置に入力する。
【００３３】
また、ユーザは、状態の切れ目となる構文ポイント、例えばAPI（ITRONのslp_tskなどイベント待ちに対応するAPI)を指定する情報である状態分割ポイント指定情報を状態遷移モデル生成装置に入力する。
状態遷移モデル生成装置は、状態遷移モデルの状態のそれぞれを、状態分割ポイント（プログラム上での位置）と、状態変数の値とで記述してゆく。
状態変数をs1~snとすると、状態は以下の記述形式で記述できる。
状態：    （状態分割ポイント, （s1の値, s2の値, …, snの値))
【００３４】
状態遷移モデル生成装置は、次状態遷移モデルを決めるのに不足する変数（補完変数）をソースコード１０から抽出する。但し、無駄な補完変数を出来る限り含ませないことが好ましい。なぜなら、無駄な補完変数を含ませることにより状態が無限になり状態遷移モデル生成が失敗する可能性が高まるからである。
【００３５】
状態遷移モデル生成装置は、状態変数の状態遷移モデルを仮想実行し、状態を網羅検索技術により抽出する。また、状態遷移モデル生成装置は、各状態分割ポイント間で起こりうる実行パスを解析して取得し、取得した実行パスの仮想実行により状態変数の変化を抽出する。
【００３６】
状態遷移モデル生成装置は、上記解析により得た状態及び状態変数の変化により、状態変数の張る空間を網羅的に解析し、解析結果から状態遷移モデル生成する。
【００３７】
[１．１．構成例]
本発明の第１の実施の形態にかかる状態遷移モデル生成装置の構成について説明する。図４は、本実施の形態に係る状態遷移モデル生成装置の構成例を示す機能ブロック図である。なお、機能ブロック図中に示す構成要素は、状態遷移モデル生成装置１の機能を機能ごとにまとめてブロックとして捉えたものであり、状態遷移モデル生成装置１が各構成要素に対応する基板、装置、回路、部品などの物理的構成要素を備えていなければならないことを意味するわけではない。また、「接続されている」とは、データ、情報、命令などの送受信、受け取り、受け渡しなどが可能な状態になっていることをいい、互いに配線で連結されているような物理的な接続に限られる意味ではない。本明細書中の他の構成要素の機能ブロック図の説明についても同様である。
【００３８】
状態遷移モデル生成装置１は、入力情報記憶部１００と、入力情報記憶部１００に接続された補完変数抽出部２００と、補完変数抽出部２００に接続された状態遷移モデル生成部３００と、状態遷移モデル生成部３００に接続された状態遷移モデル再構成部４００とを有している。補完変数抽出部２００は抽出手段に相当する。状態遷移モデル生成部３００は生成手段に相当する。状態遷移モデル再構成部４００は再構成手段に相当する。
【００３９】
［１．１．１．入力情報記憶部］
入力情報記憶部１００は、ソースコード１０と、状態変数指定情報２０と、状態分割ポイント指定情報３０とを記憶している。ソースコード１０は、状態遷移モデル生成装置１によって状態遷移モデルを生成する対象であって、手続き型言語で記述された命令文の集合である。状態変数指定情報２０は、ソースコード１０に含まれる状態変数を指定する情報である。状態分割ポイント指定情報２０は、ソースコード１０に含まれる状態分割ポイントとなる手続き（本実施の形態ではAPI）を指定する情報である。
【００４０】
［１．１．２．補完変数抽出部］
補完変数抽出部２００は、ソースコード１０から補完変数を抽出する機能を有する。
本実施の形態は、状態変数の値に注目して、状態遷移モデルを生成するものである。
状態変数をs1、s2、…、sn とすると、ある状態は以下のように、状態分割ポイントを特定する情報、各状態変数の値の組合せによって記述できる。
状態：    （状態分割ポイント, （s1の値, s2の値, …, snの値))
【００４１】
しかし、これだけの情報では状態遷移モデルが抽出できない場合がある。そのため状態を、各状態分割ポイントで補完する変数が必要なる。この補完する変数を補完変数と呼ぶ。補完変数は、各状態分割ポイント間で、状態変数の値を計算する際、必要となる変数である。補完変数抽出部２００は、ソースコード１０から補完変数を抽出する。
【００４２】
図５に状態遷移モデル生成装置１に入力されるソースコードの一部を示す。図５に示したソースコード中で使用されている変数sm、及び変数mm を状態変数としたとき、状態分割ポイントAでの補完変数はsf となる。mm=mmA 、sm=smA、sf=sfA（mmA、smA、sfAは確定した値）とすると、状態分割ポイントAから状態分割ポイントBまでのソースコードが実行されると、変数mm=mmA+1、変数sm=smA+sfA となる。変数sfを補完変数として扱うことにより、状態変数mm、smはいずれも計算できる変数となる。
【００４３】
[状態分割ポイント]
プログラムの全ての実行パス上の状態分割ポイントの並びを考える。例えば以下では、状態分割ポイントAの直後の状態分割ポイントは状態分割ポイントB となる。このように直後に並ぶ（A、B）の様な状態分割ポイントの組の集合をDivPoints とする。図６に、状態分割ポイントの並びを説明するための、ソースコードの例を示す。このソースコードでは、while文により、ループ条件が満たされるまで、状態分割ポイントA→状態分割ポイントB状態分割ポイントA→状態分割ポイントBというようになる。よって、この場合、(A,B)∈ DivPoints    (B,A)∈ DivPointsとなる。
【００４４】
[補完変数抽出]
各状態分割ポイントに、以下を満たすように、そのポイントで有効ないくつかの変数を定めたとき、この変数を補完変数と呼ぶ。
（A,B) ∈ DivPointsでなら、
状態分割ポイントAの状態変数と補完変数の値が定まっているならば、状態分割ポイントBの状態変数と補完変数の値が定まる
【００４５】
図７に、補完変数の例を説明するためのソースコードを示す。図７に示したソースコードにおいて状態変数をsmとmmであるものとすると、状態分割ポイントAでの補完変数はsfであり、状態分割ポイントBでの補完変数は無しとなる。Bの状態変数sm,mmの値は、Aの状態変数の値をsmA, mmA,補完変数の値をsfAとすると、sm= smA +1,  mm= sfAとなり、いずれの状態変数sm,mmの値も定まる。
【００４６】
［１．１．３．状態遷移モデル生成部］
状態遷移モデル生成部３００は、状態が与えられた時、その次の状態を生成してゆくことによって、ソースコード１０に対応する状態遷移モデルを生成する機能を有する。なお、ここで生成される状態遷移モデルは、補完変数を含んだ状態遷移モデルである。
ソースコード中で開始位置（一番頭の状態分割ポイント）での、状態変数、補完変数の値は求まる。
【００４７】
次に、Set = { (開始位置、状態変数、tskの値) }とする。
（１）Setからマークのないものを１つ取り出して（状態分割ポイントAとする、マークをつける）、その直後にくる、状態分割ポイントB を見つけ出す。
（２）ソースコード中の補完変数の定め方から、状態分割ポイントBでの状態変数、補完変数の値が定まる。
（３）それをSetにいれる。式で表現すると以下のようになる。
Set = Set ∪ { (B, 定まった状態変数、補完変数の値) }
（１）に戻る。
【００４８】
上記（１）から（３）を繰り返していくと、状態変数、補完変数の値域が有限離散ならば、やがて Setは全てマークがついたものになる。状態遷移モデルが完成し、状態遷移モデル生成部３００は、処理を終了する。
【００４９】
［１．１．４．状態遷移モデル再構成部］
状態遷移モデル再構成部４００は、状態遷移モデル生成部３００によって生成された状態遷移モデルを、補完変数を除いた状態変数のみの状態遷移モデルに書換え、出力する機能を有する。
【００５０】
状態遷移モデル生成部３００から出力される状態遷移モデルの状態は、状態変数だけでなく、補完変数の値を含んだ情報として生成されているので、これを変形して、状態変数の値のみでの状態遷移モデルに書換える処理を実行することにより、補完変数の値を含まない状態遷移モデルを生成し、出力する。
【００５１】
［２．動作例］
［２．１．状態遷移モデル生成処理］
次に、状態遷移モデル生成装置１の動作例を説明する。図８に、状態遷移モデル生成装置１の主たる動作である状態遷移モデル生成処理のフローチャートを掲げる。
状態遷移モデル生成処理の準備として、ユーザは、ソースコード１０、状態変数指定情報２０、状態分割ポイント指定情報３０を作成し、入力情報記憶部１００に記憶させておく。
【００５２】
状態遷移モデル生成処理において、状態遷移モデル生成装置１、より詳しくは補完変数抽出部２００は、ソースコード１０から補完変数を抽出する補完変数抽出処理を実行し（S10）、抽出した補完変数の情報を状態遷移モデル生成部３００に渡す。
【００５３】
次に、状態遷移モデル生成装置１、より詳しくは状態遷移モデル生成部３００は、網羅状態遷移モデル生成処理を実行し（S20）、網羅状態遷移モデルを生成し、状態遷移モデル再構成部４００にこれを渡す。
次に状態遷移モデル生成装置１、より詳しくは状態遷移モデル再構成部４００は、状態遷移モデル再構成処理を実行し、状態遷移モデルを出力する。
以上で状態遷移モデル生成装置１は状態遷移モデル生成処理を終了する。
【００５４】
［２．１．１．補完変数抽出処理］
上述の補完変数抽出処理（S10）の例を説明する。図９Ａ、図９Ｂに補完変数抽出処理（S10）の例を示すフローチャートを掲げる。
補完変数抽出部２００は、状態変数のIDを x1, x2, ..., xnとし、状態分割ポイントの集合をGとし、対応するtskを対応付ける 。補完変数抽出部２００は、各状態分割ポイントA∈Gに対応する初期補完変数リストをSA:={}を生成し、状態分割ポイントAの被支配状態変数書換えポイントを集合PAとする。また補完変数抽出部２００は、L=Gである集合Lを生成する（S101）。
補完変数抽出部２００は、以下の様に、各状態分割ポイントに対する状態変数リストを求める。
【００５５】
補完変数抽出部２００は、集合Lからマークのついていない状態分割ポイントAがあるか否かを判定する（S102）。マークのついていない状態分割ポイントAがあると判定した場合（S102, Yes）、状態分割ポイントAにマークをつける（S103）。一方、マークが付いている状態分割ポイントが集合Lにないと判定した場合（S102、No）、補完変数抽出部２００は補完変数抽出処理を終了する。
【００５６】
ステップS103の後、補完変数抽出部２００は被支配状態変数書換えポイントの集合PAに含まれる被支配状態変数書換えポイントpのそれぞれについて以下の処理を繰り返す（S104）。
【００５７】
次に、補完変数抽出部２００は被支配状態変数書換えポイントpに現れる変数であって、状態分割ポイントAを含んだスコープを持つ変数xの集合に含まれる変数yのそれぞれについて以下の処理を繰り返す（S105）。
【００５８】
まず、補完変数抽出部２００は変数yについて、変数ｙは被支配状態変数書換えポイントpで状態分割ポイントAと独立関連であるか否かを判定する（S106）。変数ｙは被支配状態変数書換えポイントpで状態分割ポイントAと独立関連でないと判定した場合（S106, false）、補完変数抽出部２００はステップS104に戻り、処理を続行する。一方、変数yは被支配状態変数書換えポイントpで状態分割ポイントAと独立関連であると判定した場合（S106, true）、補完変数抽出部２００は、変数yの支配変数があるか否かを判定する（S107）。変数yの支配変数がないと判定した場合（S107、false）、補完変数抽出部２００は、補完変数抽出処理が失敗したとして、補完変数抽出処理を終了する。一方、変数yの支配変数があると判定した場合（S107、true）、補完変数抽出部２００は状態変数リストSAに変数yの支配変数を追加するとともに、状態分割ポイントAのマークを削除する。
【００５９】
次に補完変数抽出部２００は変数yのスコープ内で状態分割ポイントAと連結な状態分割ポイントの集合に含まれる状態分割ポイントBのそれぞれについて以下の処理を繰り返す（S108）。
【００６０】
補完変数抽出部２００は、変数yが状態分割ポイントB及び状態分割ポイントA間で独立でなく、且つ 状態分割ポイントBの状態変数リストに変数yが含まれないか否かを判定する（S109）。変数yが状態分割ポイントB及び状態分割ポイントA間で独立であるか、又は状態分割ポイントBの状態変数リストに変数yが含まれると判定した場合（S109, false）、補完変数抽出部２００はステップS107に戻り処理を続行する。一方、変数yが状態分割ポイントB及び状態分割ポイントA間で独立でなく、且つ 状態分割ポイントBの状態変数リストに変数yが含まれないと判定した場合（S109, true）、補完変数抽出部２００は変数yの支配変数があるか否かを判定する（S110）。変数yの支配変数がないと判定した場合（S110、false）、補完変数抽出部２００は、補完変数抽出処理が失敗したとして、補完変数抽出処理を終了する。一方、変数yの支配変数があると判定した場合（S110、true）、補完変数抽出部２００は、状態分割ポイントBの状態変数リストSBに変数yの支配変数を追加するとともに、状態分割ポイントBのマークを削除する。その後、ステップS108に戻り処理を続行する。
以上で、補完変数抽出処理の説明を終了する。
【００６１】
［２．１．２．網羅状態遷移モデル生成処理］
上述の網羅状態遷移モデル生成処理（S20）の例を説明する。図１０に網羅状態遷移モデル生成処理（S20）の例を示すフローチャートを掲げる。
各状態分割ポイントに対し、補完変数抽出部２００にて状態変数リストが作成されている。また、生成される状態遷移モデルの状態sは、s={D,L} : D∈状態分割ポイント集合、L=状態変数リストに対応するその値と表されるとする。
【００６２】
プログラム開始ポイントをSPとし、プログラム開始ポイントSPでの状態変数リストをSSP=｛v1, v2, ..., vn｝、状態変数の初期値をa1, a2, ..., anとする。状態集合をns:={SP,(a1,a2,...,an)}, 遷移集合  ts:={} とする（S201）。
次に状態遷移モデル生成部３００は以下の手順で状態遷移モデルを生成する。  
【００６３】
まず、状態遷移モデル生成部３００は状態集合nsにマークが付いていない状態があるか否かを判定する（S202）。状態集合nsにマークが付いていない状態がないと判定した場合（S202, false）、状態遷移モデル生成部３００は網羅状態遷移モデル生成処理（S20）を終了する。一方、状態集合nsにマークが付いていない状態があると判定した場合（S202, true）、状態集合nsからマークがついてない状態を取り出す。これをs (=(D,L)) とする。
状態遷移モデル生成部３００は取り出した状態sにマークを付ける（S203）
次に状態遷移モデル生成部３００は状態分割ポイントDの後続の状態分割ポイントをD1,D2, …, Dpとする（S204）。
状態遷移モデル生成部３００は上記後続の状態分割ポイントD1, D2, …, Dpのそれぞれについて以下の処理を実行する（S205）。
【００６４】
状態遷移モデル生成部３００は、マークがついてない状態sに対する状態分割ポイントDからDi（Diは選択された後続状態分割ポイント）への書換えパスの集合の数が有限個か否かを判定する（S206）。書換えパスの集合の数が有限個でないと判定した場合（S206, false）、状態遷移モデル生成部３００は網羅状態遷移モデル生成処理が失敗したものとして、網羅状態遷移モデル生成処理を終了する。一方、書換えパスの集合の数が有限個であると判定した場合（S206, true）、状態遷移モデル生成部３００は遷移集合tsと状態集合nsとを生成する。
【００６５】
ここで説明のため、書き換えパスiを通るための条件を&&で書き並べたものをCik(i)、そのパスで実行される処理を；で書き並べたものをAik(i)とする（S207）。
状態分割ポイントDにて状態分割ポイントDの状態変数リストに含まれる各変数値に状態変数リストに対応するその値Lが定める値を代入して、パスPijを仮想実行した時、各状態分割ポイントDiで状態分割ポイントDiの状態変数リストの変数の値は定数となる（アルゴリズム１での状態変数リストの決め方より明らか）。状態変数リストの変数の値をLijとする。なお、「仮想実行」とは仮想実行パスP上の構文ポイントを上から順に、表されている計算・代入式の意味に従って、変数の値マップを更新する処理である。
状態遷移モデル生成部３００は上記の要素を用いて遷移集合tsと状態集合nsを以下のように生成する（S208）。
【００６６】
ts:= ts ∪ {(D,L)→[Ci1]/Ai1→(Di,Li1), (D,L)→[Ci2]/Ai2→(Di,Li2), …, (D,L)→[Cik(i)]/Aik(i)→(Di,Lik(i))}
ns:=ns ∪ (Di,Li1), (Di,Li2), …, (Di,Lik(i))
但し、状態集合nsでマークが付いているものはマークを付けたままとする。
この後、状態遷移モデル生成部３００はステップS202に戻り、網羅状態遷移モデル生成処理を継続する。
以上で網羅状態遷移モデル生成処理の説明を終了する。
【００６７】
［２．１．３．状態遷移モデル再構成処理］
上述の状態遷移モデル再構成処理（S30）の例を説明する。図１１Ａ、図１１Ｂに状態遷移モデル再構成処理（S30）の例を示すフローチャートを掲げる。
状態遷移モデル再構成部４００は、網羅状態遷移モデル生成処理によって生成された補完変数を含んだ状態遷移モデルのデータとして、ノードの集合ns1とエッジの集合ts1を取得するとともに、補完変数を含まない状態遷移モデルのデータを格納するためのノードの集合ns2とエッジの集合ts2を生成する（S301）。
ns2:={}
ts2:={}
【００６８】
次に状態遷移モデル再構成部４００は、ノードの集合ns1の要素、ノードsのそれぞれについて、以下の処理を実行する（S302）。
状態遷移モデル再構成部４００は、ノードsから補完変数の値を取り除いたものであるノードs'を集合ns2に追加して行く（S303）。式で表すと
ns2:=ns2∪{s'}
となる。
【００６９】
この追加する処理をノードの集合s1に含まれる全てのノードsについて行う（S304）。
次に状態遷移モデル再構成部４００は、集合ns2に含まれるそれぞれのノードsについて以下の処理を実行する（S305）。
まず状態遷移モデル再構成部４００は、後述するノードt'を格納するための集合Ys（例えば、構造体）を用意する（S306）。式で表すと
Ys=｛｝
である。
【００７０】
次に状態遷移モデル再構成部４００は、集合ns1に含まれるそれぞれのノードtについて以下の処理を実行する（S307）。
状態遷移モデル再構成部４００は、sはtの補完変数の値を取り除いたもの、t'はtの補完変数以外の変数の値を取り除いたものとしたとき、状態遷移モデル再構成部４００は、ノードtからノードt'sを作成し、これを集合Ysに追加する（S308）。数式で表すと
Ys:=Ys∪{t’}
となる。
【００７１】
状態遷移モデル再構成部４００は、集合ns1に含まれるそれぞれのノードtについてステップS308を繰り返す（S309）。
さらに状態遷移モデル再構成部４００は、ステップS306からS309を、集合ns2に含まれる全てのノードsについて実行する（S310）。
【００７２】
次に状態遷移モデル再構成部４００は、エッジの集合ts1に含まれるそれぞれのエッジuについて以下の処理を実行する（S311）。
【００７３】
u =s1→[C]/A→s2と記述されているものとする。状態s1の補完変数をy1, y2, …, yn、その値をa1, a2, …, an、状態s1、状態s2の補完変数の値を取り除いたものをそれぞれs'1、s'2とすると、状態遷移モデル再構成部４００は、エッジuを補完変数とその値を用いて以下のように書き換える(S312)。
s'1→[C&& y1==a1&&y2==a2&&…,&&yn==an]/A→s'2
【００７４】
次に状態遷移モデル再構成部４００は、書き換えたエッジuを集合ts2に追加して行く（S312）。式で表現すると以下のようになる。
ts2:= ts2∪{ s'1→[C&& y1==a1&&y2==a2&&…,&&yn==an]/A→s'2}
状態遷移モデル再構成部４００は、上記ステップS312を、集合ts1に含まれるすべてのノードtについて実行する（S313）。
【００７５】
次に状態遷移モデル再構成部４００は、集合ts2に含まれるエッジtの全てにマークがあるか否かを判定する（S314）。エッジtの全てにマークがあると判定した場合（S314, true）、状態遷移モデル再構成部４００は、集合ns2、集合ts2を出力して状態遷移モデル再構成処理を終了する。一方、エッジtの全てはマークがないと判定した場合（S314, false）、状態遷移モデル再構成部４００は、集合ts2からマークのない元（エッジt）を一つ取り出す（S315）。取り出したエッジをエッジu0とする。状態遷移モデル再構成部４００は、エッジu0にマークを付ける。
【００７６】
u0=s1→[C&& y1==a1&&y2==a2&&…,&&yn==an]/A→s2 とする。状態遷移モデル再構成部４００は、エッジu0とa1, a2, … ,anの部分だけが違うエッジ（s1, C, A, s2の部分は共通）を、集合ts2から集める。
集めたエッジu1、u2、…、ukが以下の内容であるとすると、
u1=s1→[C&& y1==a11&&y2==a21&&…,&&yn==an1]/A→s2,
u2=s1→[C&& y1==a12&&y2==a22&&…,&&yn==an2]/A→s2,
… ,  
uk=s1→[C&& y1==a1k&&y2==a2 k &&…,&&yn==ank]/A→s2
【００７７】
状態遷移モデル再構成部４００は、前述のステップS305からS310において生成した集合Ys1S ={( a11,a21,…,an1), (a12,a22,…,an2) ,…, (a1k,a2k,…,ank)}ならば、ts2からu1,u2,…, ukを全て取り除き、代わりに s1→[C]/A→s2を入れ、これにマークをつける（S316)。
この後状態遷移モデル再構成部４００は、ステップS314に戻り、処理を繰り返す。
以上で状態遷移モデル再構成処理の説明を終了する。
【００７８】
［１．３．実施例］
上記第１の実施の形態の実施例を示す。図１２Ａ、図１２Ｂ、図１２Ｃ、図１２Ｄに、本実施の形態に係る状態遷移モデル生成装置１で状態遷移モデルを生成させるソースコードを示す。
状態遷移モデル生成装置１は、図１２Ａから図１２Ｄに示したソースコードから状態遷移モデルを生成するものとする。
【００７９】
初期状態変数をmm, smとする情報を、状態遷移モデル生成装置１、より詳しくは入力情報記憶部１００に状態変数指定情報２０として、記憶させる。また、状態分割ポイント指定情報３０を状態遷移モデル生成装置１、より詳しくは入力情報記憶部１００に記憶させる。
この時、状態分割ポイントは、ソースコード１０中の状態分割ポイントA,B,C,Dとなる。
【００８０】
また、状態変数書き換えポイントは、1A, 2B, 3B, 4B, 5B, 6B, 7C, 8C, 9C, 10B, 11D, 12D, 13Dとなる。最後の英字はその支配分割ポイントを表す。
【００８１】
なお、図１２Ａから図１２Ｄに示すソースコード中に状態分割ポイントA,B,C,D、及び状態変数書き換えポイント1A, 2B, 3B, 4B, 5B, 6B, 7C, 8C, 9C, 10B, 11D, 12D, 13Dを示すコメント行を記したが、ソースコード１０中にこのような記述を付加する必要があるわけではない。
【００８２】
上記ソースコード１０から補完変数抽出部２００は、状態分割ポイントA,B,C,Dの状態変数と補完変数を以下のように抽出する。
SA={mm,sm}
SB={mm,sm,sf}
SC={mm,sm}
SD={mm,sm,sf}
【００８３】
上記の状態分割ポイントA,B,C,Dの状態変数と補完変数から、状態遷移モデル生成部３００は、図１３Ａ、図１３Ｂ、図１３Ｃに示す網羅状態遷移モデルを生成する。図１３Ａは図１２Ａから図１２Ｄに示したソースコードから状態遷移モデル生成部３００が生成した網羅状態遷移モデルのデータ例を示す図、図１３Ｂは図１３Ａに続く網羅状態遷移モデルのデータ例を示す図、図１３Ｃは図１３Ｂに続く網羅状態遷移モデルのデータ例を示す図、図１３Ｄは図１３Ｃに続く網羅状態遷移モデルのデータ例を示す図である。
図１４は、図１３Ａ、図１３Ｂ、図１３Ｃに示す網羅状態遷移モデルのデータから生成されるステートチャートの例である。
【００８４】
状態遷移モデル再構成部４００は、図１３Ａ、図１３Ｂ、図１３Ｃに示す網羅状態遷移モデルのデータから、状態に補完変数を含まない状態遷移モデルのデータ５００を生成する。図１５Ａは図１３Ａから図１３Ｃに示した網羅状態遷移モデルのデータから状態遷移モデル再構成部４００が生成した、補完変数を含まない状態遷移モデルのデータ例を示す図、図１５Ｂは図１５Ａに続く状態遷移モデルのデータ例を示す図である。
【００８５】
図１６は、図１３Ａ、図１３Ｂ、図１３Ｃに示す網羅状態遷移モデルのデータから生成されるステートチャートの例である。図１６に示すステートチャートは、状態に状態変数mm, msの値のみがあり、補完変数sf及びその値は、エッジの[条件]に記述される。その結果として、状態変数mm, msの値のそれぞれは同じであるが、補完変数sfの値が異なっていた複数の状態は、一つの状態に集約される。すなわち、図１４の状態B[1,5,2]、状態B[1,5,3]は、図１６では一つの状態B[1,5]に集約され、図１４の状態B[1,1,2]、状態B[1,1,3]は、図１６では一つの状態B[1,1]に集約され、図１４の状態D[1,4,2]、状態D[1,4,3]は、図１６では一つの状態D[1,4]に集約される。補完変数を含まない状態A[0,5]、C[1,2]、C[1,3]は、そのままとなっている。
【００８６】
［４．第２の実施の形態］
本発明の第２の実施の形態を説明する。第２の実施の形態は状態遷移モデル生成装置２として提案される。図１７は、本実施の形態に係る状態遷移モデル生成装置の構成例を示す機能ブロック図である。
【００８７】
［４．１．構成例］
状態遷移モデル生成装置２は、入力情報記憶部１００と、入力情報記憶部１００に接続された補完変数抽出部２００と、補完変数抽出部２００に接続された補完変数値域抽出部６００と、補完変数値域抽出部６００に接続された補完変数離散値パス分解部７００と、補完変数離散値パス分解部７００に接続された状態遷移モデル生成部３００とを有している。補完変数値域抽出部６００は計算手段に相当する。補完変数離散値パス分解部７００は書き換え手段に相当する。
【００８８】
この状態遷移モデル生成装置１は、手続き型言語によって記述されたソースコードに含まれる、状態を表す変数（状態変数）を用いて状態遷移モデルを生成する装置である。
【００８９】
状態遷移モデル生成装置２は、情報処理装置であって、この情報処理装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読み出し専用メモリ（ROM）、入出力装置（Ｉ／Ｏ）、及び必要な場合にはハードディスク装置等の外部記憶装置を具備している装置である。
【００９０】
［４．１．１．入力情報記憶部］
入力情報記憶部１００は、第１の実施の形態と同様であるので、同一の構成要素には同一の参照符号を付してそれらの詳細な説明は省略する。
【００９１】
［４．１．２．補完変数抽出部］
補完変数抽出部２００は、第１の実施の形態と同様であるので、同一の構成要素には同一の参照符号を付してそれらの詳細な説明は省略する。
【００９２】
［４．１．３．補完変数値域抽出部］
補完変数値域抽出部６００は、各状態分割ポイントでの補完変数の値域を取得する機能を有する。補完変数の地域を取得する処理は、第1の実施の形態のステップS207における処理と同様である。
【００９３】
［４．１．４．補完変数離散値パス分解部］
補完変数離散値パス分解部７００は、補完変数を書換えポイントから消去する機能を有する。補完変数の値域が離散有限であるとき、補完変数に対する条件分岐命令により、値域分の実行パスに分割し、補完変数の値の書き換えポイントでは補完変数を具体的な値域に置き換えるように、ソースコードを書き換える。この処理によって、ソースコード１０中の書き換えポイントから補完変数を消去する。
【００９４】
［４．１．５．状態遷移モデル生成部］
状態遷移モデル生成部３００は、第１の実施の形態と同様であるので、同一の構成要素には同一の参照符号を付してそれらの詳細な説明は省略する。但し、補完変数離散値パス分解部７００によって出力される、書き換えられたソースコードには補完変数が具体的な値域に置き換えられているので、第2の実施の形態における状態遷移モデル生成部３００は、補完変数を含まない状態生成モデルのデータを出力する。
【００９５】
［４．３．動作例］
次に、第２の実施の形態にかかる状態遷移モデル生成装置２の動作例を説明する。図２２に、状態遷移モデル生成装置２の主たる動作である状態遷移モデル生成処理のフローチャートを掲げる。
【００９６】
状態遷移モデル生成処理の準備として、ユーザは、ソースコード１０、状態変数指定情報２０、状態分割ポイント指定情報３０を作成し、入力情報記憶部１００に記憶させておく。
【００９７】
状態遷移モデル生成処理において、状態遷移モデル生成装置１、より詳しくは補完変数抽出部２００は、ソースコード１０から補完変数を抽出する補完変数抽出処理を実行し（S410）、抽出した補完変数の情報を補完変数値域抽出部６００に渡す。
【００９８】
状態遷移モデル生成装置２、より詳しくは補完変数値域抽出部６００は、ソースコード１０を解析して各状態分割ポイントでの補完変数の値域を取得する処理である補完変数値域抽出処理を実行する（S420）。
【００９９】
次に状態遷移モデル生成装置２、より詳しくは補完変数離散値パス分解部７００は、補完変数の値の書き換えポイントでは補完変数を具体的な値域に置き換える補完変数離散値パス分解処理を実行する（S430）。状態遷移モデル生成装置２、より詳しくは補完変数離散値パス分解部７００は、補完変数を具体的な値域に置き換えたソースコード１０を状態遷移モデル生成部３００に渡す。
【０１００】
次に状態遷移モデル生成装置２、より詳しくは状態遷移モデル生成部３００は、補完変数を具体的な値域に置き換えたソースコード１０から状態遷移モデルのデータ５００を生成する処理である状態モデル生成処理を実行する（S440）。状態モデル生成処理実行の結果として、状態遷移モデル生成装置２、より詳しくは状態遷移モデル生成部３００は、補完変数を状態に含まない状態モデルのデータ５００を出力する。
以上で、状態遷移モデル生成装置２は状態遷移モデル生成処理を終了する。
【０１０１】
［４．４．実施例］
上記第２の実施の形態の実施例を示す。図１８Ａ、図１８Ｂ、図１８Ｃ、図１８Ｄ、図１８Ｅに、本実施の形態に係る状態遷移モデル生成装置１で状態遷移モデルを生成させるソースコード１０を示す。
状態遷移モデル生成装置１は、図１８Ａから図１８Ｅに示したソースコードから状態遷移モデルを生成する。
【０１０２】
初期状態変数をmm, sm とする情報を、状態遷移モデル生成装置１、より詳しくは入力情報記憶部１００に状態変数指定情報２０として、記憶させる。また、状態分割ポイント指定情報３０を状態遷移モデル生成装置１、より詳しくは入力情報記憶部１００に記憶させる。
この時、状態分割ポイントは、ソースコード１０中の状態分割ポイントA,B,C,Dとなる。
【０１０３】
また、状態変数書き換えポイントは、1A, 2B, 3B, 4B, 5B, 6B, 7C, 8C, 9C, 10B, 11D, 12D, 13Dとなる。最後の英字はその支配分割ポイントを表す。
【０１０４】
なお、図１８Ａから図１８Ｅに示すソースコード中に状態分割ポイントA,B,C,D、及び状態変数書き換えポイント1A, 2B, 3B, 4B, 5B, 6B, 7C, 8C, 9C, 10B, 11D, 12D, 13Dを示すコメント行を記したが、必ずしもソースコード１０中にこのような記述を付加する必要があるわけではない。
【０１０５】
上記ソースコード１０から補完変数抽出部２００は、状態分割ポイントA,B,C,Dの状態変数と補完変数を以下のように抽出する。
SA={mm,sm}
SB={mm,sm,sf}
SC={mm,sm}
SD={mm,sm,sf}
【０１０６】
次に補完変数値域抽出部６００は、第1の実施の形態にかかる状態遷移モデル生成部３００と同様に、状態遷移モデルのデータを生成し、このデータからそれぞれの状態分割ポイントにおける補完変数sfの値を取得する。本実施例では、補完変数値域抽出部６００は状態分割ポイントの B,Dのsfの値域を
B：sf=2,3
D : sf= 2,3
と抽出する。
【０１０７】
次に補完変数離散値パス分解部７００は、ソースコード１０を、補完変数に対する条件分岐命令により、値域分の実行パスに分割し、ソースコード１０中の補完変数の値の書き換えポイントでは補完変数を具体的な値域に書き換える。
【０１０８】
図１９Ａから図１９Ｄに、補完変数離散値パス分解部７００によって書き換えられたソースコードの例を示す。補完変数離散値パス分解部７００によって書き換えられた部分は、図１９Ｂのコード１９００の部分である。これはコード「sm=sf」が補完変数離散値パス分解部７００によって書き換えられたものである。
【０１０９】
次に状態遷移モデル生成部３００は、補完変数離散値パス分解部７００によって書き換えられたソースコードから状態遷移モデルのデータ５００を生成する。生成される状態遷移モデルのデータ５００は、第１の実施の形態の状態遷移モデル再構成部４００から出力されるものと同一の内容となる。
【０１１０】
図２０Ａ、図２０Ｂに状態遷移モデル生成部３００によって生成される状態遷移モデルのデータ５００の例を示し、図２１に図２０Ａ、図２０Ｂに示した状態遷移モデルのデータ５００から生成されるステートチャートの例を示す。図２１に示すステートチャートは、状態に状態変数mm, msの値のみがあり、補完変数sf及びその値は、エッジの[条件]に記述される。
【０１１１】
［５．利点］
本発明によれば、手続き型言語で記述されたソースコードから状態遷移モデルを取り出すことができる。取り出した状態遷移モデルを解析することで、設計を理解すること、さらに取り出した状態遷移モデルを修正し、改良、新たな設計を開始することも可能となる。
【０１１２】
[６．まとめ、その他]
以上、本発明の実施の形態を説明したが、本発明はこれらに限定されるものではなく、発明の趣旨を逸脱しない範囲内において、種々の変更、追加、組み合わせ等が可能である。
【符号の説明】
【０１１３】
１、２・・・状態遷移モデル生成装置；  １００・・・入力情報記憶部；  ２００・・・補完変数抽出部；  ３００・・・状態遷移モデル生成部；  ４００・・・状態遷移モデル再構成部；  ５００・・・状態遷移モデルデータ；  ６００・・・補完変数値域抽出部；  ７００・・・補完変数離散値パス分解部；
【図１】
2015069617.tif 000003
【図２】
2015069617.tif 000004
【図３】
2015069617.tif 000005
【図４】
2015069617.tif 000006
【図５】
2015069617.tif 000007
【図６】
2015069617.tif 000008
【図７】
2015069617.tif 000009
【図８】
2015069617.tif 000010
【図９Ａ】
2015069617.tif 000011
【図９Ｂ】
2015069617.tif 000012
【図１０】
2015069617.tif 000013
【図１１Ａ】
2015069617.tif 000014
【図１１Ｂ】
2015069617.tif 000015
【図１２Ａ】
2015069617.tif 000016
【図１２Ｂ】
2015069617.tif 000017
【図１２Ｃ】
2015069617.tif 000018
【図１２Ｄ】
2015069617.tif 000019
【図１３Ａ】
2015069617.tif 000020
【図１３Ｂ】
2015069617.tif 000021
【図１３Ｃ】
2015069617.tif 000022
【図１４】
2015069617.tif 000023
【図１５Ａ】
2015069617.tif 000024
【図１５Ｂ】
2015069617.tif 000025
【図１６】
2015069617.tif 000026
【図１７】
2015069617.tif 000027
【図１８Ａ】
2015069617.tif 000028
【図１８Ｂ】
2015069617.tif 000029
【図１８Ｃ】
2015069617.tif 000030
【図１８Ｄ】
2015069617.tif 000031
【図１８Ｅ】
2015069617.tif 000032
【図１９Ａ】
2015069617.tif 000033
【図１９Ｂ】
2015069617.tif 000034
【図１９Ｃ】
2015069617.tif 000035
【図１９Ｄ】
2015069617.tif 000036
【図２０Ａ】
2015069617.tif 000037
【図２０Ｂ】
2015069617.tif 000038
【図２１】
2015069617.tif 000039
【図２２】
2015069617.tif 000040