(57)【要約】      （修正有）【課題】状態変数を自動的にかつ的確に特定できるソフトウエア検証用システムを提供する。【解決手段】ソフトウエア検証用システムは、状態変数候補抽出部２１、条件式抽出部２２、数値化部２３、及び状態変数決定部２４を備える。状態変数候補抽出部は、ソースコード中に含まれる変数の各々に着目し、その変数が何らかの定数と比較されている箇所の数を計数し、その数が閾値を超えた場合、その変数を状態変数候補情報として出力し記憶する。条件式抽出部は、状態変数候補である変数が現れる条件式を抽出するとともに、当該変数がどのような形で現れるかに関する情報を条件式情報として出力する。数値化部は、条件式抽出部で抽出された条件式情報に基づき、状態変数候補である変数のそれぞれにつき数値化を行い、その数値を数値化情報として出力する。状態変数決定部は、数値化情報に基づき、状態変数候補である変数の中から状態変数となるべき変数を決定する。【選択図】図３
2018049565.tif 000002
【特許請求の範囲】
【請求項１】
状態変数の候補となる変数を抽出する状態変数候補抽出部と、
前記変数が含まれる条件式を抽出する条件式抽出部と、
前記条件式における前記変数の現れ方を数値化し、その数値化の結果に基づいて、前記状態変数候補抽出部で抽出された前記変数の中から状態変数を決定する状態変数決定部と
を備えたことを特徴とするソフトウエア検証用システム。
【請求項２】
前記状態変数決定部は、
前記条件式抽出部で抽出された複数の条件式の各々において、一の変数以外の変数の種類の数を特定し、その数に基づいて前記一の変数の第１の特性を数値化する、請求項１記載のソフトウエア検証用システム。
【請求項３】
前記状態変数決定部は、
前記変数がとり得ると推定される値の集合と、前記変数が前記実際に取る値の集合とを比較し、その比較結果に基づいて前記変数の第２の特性を数値化する、請求項１又は２記載のソフトウエア検証用システム。
【請求項４】
前記状態変数決定部は、
一の変数が含まれる条件式の各々において、その条件式を真にする前記一の変数の値の個数を特定し、その個数に基づいて、前記一の変数の第３の特性を数値化する、請求項１乃至３のいずれかに記載のソフトウエア検証用システム。
【請求項５】
状態変数の候補となる変数を抽出するステップと、
前記変数が含まれる条件式を抽出するステップと、
前記条件式における前記変数の現れ方を数値化し、その数値化の結果に基づいて、抽出された前記変数の中から状態変数を決定するステップと
を備えたことを特徴とするソフトウエア検証用方法。
【請求項６】
前記状態変数を決定するステップは、
抽出された複数の条件式の各々において、一の変数以外の変数の種類の数を特定し、その数に基づいて前記一の変数の第１の特性を数値化する、請求項５記載のソフトウエア検証用方法。
【請求項７】
前記状態変数を決定するステップは、
前記変数がとり得る値の集合と、前記変数が前記実際に取る値の集合とを比較し、その比較結果に基づいて前記変数の第２の特性を数値化する、請求項５又は６記載のソフトウエア検証用方法。
【請求項８】
前記状態変数を決定するステップは、
一の変数が含まれる条件式の各々において、その条件式を真にする前記一の変数の値の個数を特定し、その個数に基づいて、前記一の変数の第３の特性を数値化する、請求項５乃至７のいずれかに記載のソフトウエア検証用方法。
【発明の詳細な説明】
【技術分野】
【０００１】
以下に記載の実施形態は、ソフトウエア検証用システム及びソフトウエア検証方法に関する。
【背景技術】
【０００２】
ソフトウエアのソースコードを読み解いて検証するための検証システムでは一般に、ソフトウエアからグラフなどを生成し可視化することで、システムの理解を助けようとする研究が行われている。
【０００３】
しかし、従来の研究の多くは、例えば制御をモード毎に纏めたり切り離したりする際に起点となる変数（状態変数）を人手で指定したり、検証に必要な各種データを人手で選択し入力する必要がある。そのため、適切な検証結果を得るためには、検証対象のシステムやソフトウエアについて深い理解が必要であるとともに、人手による分析が必要である。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２０１３−２２２３２７号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
以下に記載の実施形態は、状態変数を自動的にかつ的確に特定することができるソフトウエア検証用システム及びソフトウエア検証方法を提供するものである。
【課題を解決するための手段】
【０００６】
一の実施形態に係るソフトウエア検証用システムは、状態変数の候補となる変数を抽出する状態変数候補抽出部と、変数が含まれる条件式を抽出する条件式抽出部と、条件式における変数の現れ方を数値化し、その数値化の結果に基づいて、状態変数候補抽出部で抽出された変数の中から状態変数を決定する状態変数決定部とを備えたことを特徴とする。
【図面の簡単な説明】
【０００７】
【図１】いわゆるハイブリッドシステムの構成を示す概念図である。
【図２】ハイブリッドシステムの特徴を説明する概念図である。
【図３】第１の実施の形態のソフトウエア検証システムの構成を示す機能ブロック図である。
【図４】第１の実施の形態のソフトウエア検証システムの動作を示すフローチャートである。
【図５】第１の実施の形態のソフトウエア検証システムを実現するハードウエア構成を示すブロック図である。
【図６】状態変数抽出部２１の機能について詳しく説明する概念図である。
【図７】条件式抽出部２２で得られた条件式テーブルの一例である。
【図８】変数の「埋没度」の概念について説明する概念図である。
【図９】変数の「不連続度」の概念について説明する概念図である。
【図１０】変数の「非独立度」の概念について説明する概念図である。
【図１１】埋没度の具体的な計算方法を説明する概念図である。
【図１２】第２の実施の形態のソフトウエア検証システム（不連続度の算出）の動作を示す概念図である。
【図１３】第３の実施の形態のソフトウエア検証システム（非独立度の算出）の動作を示す概念図である。
【図１４】第３の実施の形態のソフトウエア検証システム（非独立度の算出）の動作を示す概念図である。
【図１５】第３の実施の形態のソフトウエア検証システム（非独立度の算出）の動作を示す概念図である。
【図１６】第３の実施の形態のソフトウエア検証システム（非独立度の算出）の動作を示す概念図である。
【発明を実施するための形態】
【０００８】
以下、図面を参照して実施形態に係るソフトウエア検証システムについて説明する。このソフトウエア検証システムは、例えばハイブリッドシステムなどの物理情報システムを制御するためのソフトウエアを検証するためのシステムである。以下では、ハイブリッドシステム用のソフトウエアの検証システムを例として説明するが、これはあくまでも一例である。他の種類の物理情報システムを対象とした場合でも、ソフトウエア検証システムの構成は略同一である。したがって、本実施の形態の適用範囲は、ハイブリッドシステムに限定されるものではない。
【０００９】
［第１の実施形態］
図１は、いわゆるハイブリッドシステムの構成を示す概念図である。ハイブリッドシステムとは、物理情報システムの一例であり、例えば速度や温度のような物理量を表す連続値と、レジスタの値やメモリアドレスのようなソフトウエアの動作に関わる離散値とが相互に影響し、連続値による制御が、ある条件に従って離散値による制御に切り替わることで制御が実現されるシステムである。
図１の左側に示すように、ハイブリッドシステムは、複数のモード（例えばモード０〜３）を有しており、モードの各々において異なる連続値による制御が実行されるように構成される。そして、各モードは、図１の右側に示すように、ある条件に従って離散的に切り替わる。
【００１０】
このようなハイブリッドシステムを制御するソフトウエアのソースコードは、図２に示すように、ある１つのモードの実行時に実行される演算がソースコード上の複数の箇所に散在していたり、あるいは、図２に示すように、異なる複数のモードで実行される演算が、１つのサブルーチンの中に束ねられていたりすることもある。このようなソースコードを読み解くには、複数の箇所に散在した演算をモードと対応させて纏めたり、又は束ねられた演算をモード毎に切り離したりすることにより、個々のモード毎に実行される制御がグラフなどにより表現されることにより、視覚的に確認できる（可視化）ことが望ましい。こうすることで、ハイブリッドシステムの理解を助けることができる。
【００１１】
このようなソースコードの検証を行う場合に重要となるのが、モードを切り替える場合において起点となる変数（状態変数）の特定である。従来の各種研究では、この状態変数を人手で判断し、指定する必要がある。本実施の形態では、この状態変数を以下に説明する方法により、人手によらずに自動的に特定することができる。
【００１２】
図３は、第１の実施の形態に係るソフトウエア検証システムの動作を示す機能ブロック図である。このシステムは、状態変数候補抽出部２１、条件式抽出部２２、数値化部２３、及び状態変数決定部２４を備えている。また、図４は、このシステムの動作の手順の概略を示すフローチャートである。以下、各部２１〜２４の役割及び動作を順に説明する。
【００１３】
状態変数候補抽出部２１は、ソースコード中に含まれる変数の各々に着目し、その変数が何らかの定数と比較されている場合、その比較されている箇所の数を計数する。そして、その比較されている箇所の数が閾値を超えた場合、状態変数候補抽出部２１は、その変数を状態変数候補と認定し、その認定された変数を「状態変数候補情報」として出力し記憶する（図４のステップＳ１）。なお、閾値との比較は省略し、発見された変数はすべて状態変数候補とすることも可能である。あるいは、閾値を設定する代わりに、定数と比較されている箇所の数を変数ごとに記憶しておき、その数の大小を変数間で比較することで、状態変数候補となる変数を特定することもできる。
【００１４】
条件式抽出部２２は、状態変数候補である変数が現れる条件式（ｉｆ文、ｅｌｓｅ節など）を抽出するとともに、それら抽出された条件式において当該変数がどのような形で現れるかに関する情報を「条件式情報」として出力する（ステップＳ２）。
【００１５】
数値化部２３は、条件式抽出部２２で抽出された条件式情報に基づき、状態変数候補である変数のそれぞれにつき数値化を行い、その数値を数値化情報として出力する（ステップＳ３）。そして、状態変数決定部２４は、数値化情報に基づき、状態変数候補である変数の中から状態変数となるべき変数を決定する（ステップＳ４）。
【００１６】
図５は、このソフトウエア検証システムを実現するためのハードウエア構成を示すブロック図である。このソフトウエア検証システムは、一例として、ＣＰＵ１１、データ入力部１２、インタフェース（Ｉ／Ｏ）１３、１４、出力装置１５、ＲＯＭ１６、ＲＡＭ１７、及びハードディスクドライブ１８を備えたコンピュータにより実現され得る。例えばハードディスクドライブ１８に、図３に示すシステムを実現するためのコンピュータプログラムを格納することができる。ソースコードはデータ入力部１２から入力され、前述の状態変数候補情報、条件式情報、数値化情報、及び決定された状態変数は、ＲＡＭ１７等に記憶された後、出力装置１５から出力され得る。
なお、図５のハードウエア構成はあくまでも一例である。また、図５のようなハードウエア構成が単体の装置により実現される必要は無く、物理的に分割された複数の装置や、ネットワークにより接続された装置により、図３及び図４の動作が実現されてもよい。
【００１７】
次に、図６を参照して、状態変数候補抽出部２１の機能について詳しく説明する。図６は、一例として、通常モード制御、省エネモード制御、緊急時モード制御などを備えたエアコン制御用のソフトウエアを例として示している。それぞれの制御は、更に複数の制御に分割されている。
図６に示すように、状態変数候補抽出部２１は、ソースコード中から、１つの変数、例えば変数ａを抽出する。そして、図５の左側に示すように、変数ａが何等かの定数と比較されている箇所の数をすべて特定する。この変数ａは、ソースコード中の条件式に多数含まれているとともに、各種制御を切り替える場合の判断に用いられている。変数ａが定数と比較されている箇所の数が閾値よりも多い場合には、その変数ａを状態変数候補として抽出する。以下、ソースコード中の全ての変数について同様の判定を行い、状態変数候補を抽出する。以下の説明では、５種類の変数ａ〜ｅが抽出された場合を例として説明するが、これはあくまでも一例である。
【００１８】
条件式抽出部２２は、状態変数候補抽出部２１で抽出された状態変数候補としての各種変数が含まれる条件式を抽出する。そして、その抽出された条件式において、状態変数候補としての各種変数がどのような現れ方をするのかに関する情報を抽出する。
【００１９】
図７は、抽出された条件式の番号、その条件式に含まれる変数ａ〜ｅ、及び各条件式における変数ａ〜ｅの現れ方（どのような形で定数と比較されているか）を示す条件式テーブルである。このようなテーブルを生成するのが、条件式抽出部２２の役割である。１つの条件式において、演算子ＯＲで接続された複数の行が存在する場合、その条件式は複数行に分割して表示されている。図７の例では、条件式５及び１５が２行に分割して表示され、合計で１８個の条件式（行）が表示されている。なお、図７は、説明の簡略化のため、条件式の数を１８個としているが、これはあくまでも一例であることは言うまでもない。
【００２０】
図７の例の場合、抽出された条件式１〜１６において、状態変数候補としての５種類の変数ａ〜ｅが含まれ、それぞれの条件式においてそれら変数ａ〜ｅの「現れ方」が互いに異なっている。この第１の実施の形態では、この現れ方を以下の方法で数値化することで、複数の変数の中から状態変数を決定する。
例えば、ある条件式では、１つの変数のみが現れる場合もある一方、他の式では複数種類の変数が現れる場合がある。図８を参照して具体的に説明する。この例では、ソフトウエアに含まれる制御として制御Ａ、Ｂ、Ｃがあり、条件式に基づく判定により制御Ａ、Ｂ、Ｃのいずれかに切り替わる場合を示している。この場合、制御Ａへの切り替えは、変数ａ及びｂを含む条件式１が真（True）となった場合に行われる。この条件式１は、変数ａの影響のみで真とされるのではなく、ｂの値にも依存して真となり、変数ａの影響は相対的に小さい。同様に、制御Ｃへの切り替えは、変数ａ、ｃを含む条件式３が真となった場合に行われる。この条件式３は、変数ａの影響のみで真とされるのではなく、ｃの値にも依存して真となり、変数ａの影響は相対的に小さい。
【００２１】
これに対し、条件式２では、変数ａのみによって条件式２が真となり、その意味で変数ａの影響力が大きい。このような、ある変数（例えば変数ａ）が条件式の中で他の変数（例えば変数ｂ〜ｅ）に影響されず存在感を示しているか、それとも埋没しているのかを示す数値を、本実施の形態では「埋没度」と称する。埋没度は、数値化部２３で数値化され、状態変数決定部２４において状態変数を決定するファクターの１つとして用いられる。「埋没度」の具体的な計算方法の例は、後述する。
【００２２】
変数の現れ方を表現する尺度としては、埋没度以外にも、例えば「不連続度」も採用し得る。例えば、ある変数はソースコード中で様々な値を連続的にとり得る一方で、別の変数は特定の値しか取らなかったり、又は不連続な、飛び飛びの値しかとらなかったりする場合がある。これを図９を参照して具体的に説明する。変数ａを含む条件式があり、それぞれ制御Ａ、．．．Ｂ、Ｃへの切り替えにおいて用いられているとする。この場合、変数ａは、０、１、２、３という連続の値を取り得ると推定されるところ、実際にソースコード中を探索すると、変数ａが「１」の値を取る場合に切り替わる制御は、当該ソースコード中には存在しない、という場合がある。この場合、変数ａは、「１」の値に関しては不連続であると考えられる。このような、ある変数が不連続、換言すれば飛び飛びになる度合を、本実施の形態では「不連続度」と称する。
【００２３】
変数の現れ方を表現する更に別の尺度としては、「非独立度」も採用し得る。「非独立度」は、ある変数が登場する条件式において、その条件式を真とするような当該変数の値がどれだけ多く存在するかを示す尺度である。例えば、図１０に示すように、変数ａを含む条件式があり、変数ａの値が０の場合に制御Ａが実行される一方、変数ａの値が１の場合には制御Ｂが実行されるとする。しかし、制御Ａと制御Ｂには、どちらの場合にも実行される小制御ＡＢが含まれている。これは、小制御ＡＢは、変数ａの値が０であっても１であっても実行されることを意味する。ある変数に関し、条件式を真にする当該変数の値がどれだけ多く存在するかに関する尺度を、本実施の形態では、「非独立度」と称する。「非独立度」の具体的な計算方法の例は、後述する。
【００２４】
このように、変数の「現れ方」を表現する尺度は、「埋没度」、「不連続度」、「非独立度」など、様々なものが考えられ得る。「埋没度」、「不連続度」、及び「非独立度」（第１乃至第３の特性）は、変数の現れ方を表現する尺度の一例である。このうち、第１の実施の形態の数値化部２３では、条件式中での変数の「現れ方」を、「埋没度」の観点から数値化し、状態変数を決定する。以下、埋没度の具体的な計算方法の例を説明する。
【００２５】
埋没度の具体的な計算方法の一例を、図１１を参照して説明する。ここでは、変数ａの埋没度を計算する場合の例を示している。他の変数に関しても計算方法は同様である。
この図１１の例では、変数ａの埋没度を、抽出された条件式（行）１〜１５（２）の集合Ｐにおいて、集合Ｐ中に含まれる条件式に含まれる変数ａ以外の変数の個数（累計）に基づいて計算する。すなわち、変数ａの埋没度の計算においては、最初に、図１１に示すように、条件式抽出部２２で抽出された条件式の中からち、変数ａが含まれる条件式の行のみを更に抽出する。そして、各条件式の行において（条件式１５については、変数ａが登場する行が２行あるため、２つの条件式１５（１）、（２）に分割している）、変数ａのみが含まれている行には数値「０」を付与し、変数ａ以外の変数ｂ、ｃ、ｄ、ｅのいずれかが含まれている行には、当該それ以外の変数の種類の数を付与する。例えば、条件式１、２、７、１３には、変数ａ以外の変数が含まれていないので、数値として「０」を付与する。また、条件式４、８、９には、変数ａ以外の変数がそれぞれ１つ含まれているので数値「１」を付与する。条件式１５（１）及び１５（２）には、数値「２」が付与される。数値化部２３は、こうして各条件式（行）に付与された数値の合計（０＋０＋１＋０＋１＋１＋０＋２＋２＝７）を「埋没度」として算出する。この埋没度の数値が大きいほど、その変数は他の変数に対し相対的に埋没しており、存在感が薄く、状態変数らしさが小さいことを示す。
以上のような埋没度の演算を、変数ａだけでなく、状態変数候補抽出部２１で抽出された他の全ての変数ｂ〜ｅについても実行する。そして、状態変数決定部２４は、変数ごとに演算された埋没度を比較して、変数ａ〜ｅの中から状態変数を選択する。上述の計算方法の場合、埋没度が最も小さい変数が状態変数として選択される。
【００２６】
［効果］
以上説明したように、第１の実施の形態のソフトウエア検証システムによれば、検証の対象であるソースコードから抽出された条件式及び変数に基づき変数の埋没度を演算し、その演算結果に基づいて状態変数を特定することができる。ソースコードを入力すること以外に、人手によるデータの入力は不要であり、状態変数の特定は、人手による分析によらず自動的に、かつ的確に、しかも短時間で特定することができる。
【００２７】
［第２の実施の形態］
次に、第２の実施の形態に係るソフトウエア検証システムを、図１２を参照して説明する。この第２の実施の形態の基本的な構成及び動作は、第１の実施の形態と同一である（図３〜図５）。ただし、この実施の形態では、上述した「不連続度」の数値化を行い、その結果に基づいて状態変数を決定する。「不連続度」は、数値化部２３で数値化され、状態変数決定部２４において状態変数を決定するファクターとして用いられる。状態変数候補抽出部２１、及び条件式抽出部２２の動作は第１の実施の形態と同一である。
【００２８】
続いて、不連続度の具体的な計算方法の一例を説明する。
変数ａがとり得る値の集合を推定するとともに、変数ａがとり得る値の集合を、ソースコードを実際に探索し特定する。その推測される集合に含まれる値の数と、実測に基づく集合に含まれる値の数との割合を、変数ａの不連続度と定義することができる。具体的には、各条件式の中で［ａ＝＝ｉ］（ｉは任意の数）の表現をすべて抽出し、このｉの種類の数を特定して実測値とする。また、推定値は、このようにして得られた実測値の数値列から、不自然に飛び飛びとなった部分を補完することにより得られる。
【００２９】
より具体的に説明すると、以下のようになる。
例えば、変数ａがとり得る値ν（実測）をすべて求めて、降順（又は昇順）に並び替える。ここでは、νの値として、例えば降順に並んだ値ν０、ν１、ν２、・・・、νｎ−１、νｎが得られたものとする。
このとき、隣接する２つの値の差分値ｄｉｆｆｉ＝νｉ＋１−νｉ（ｉ＝０〜ｎ−１）を算出する。そして、得られた差分値ｄｉｆｆ０〜ｄｉｆｆｎ−１の中で最小値ｄｉｆｆｍｉｎ（＝ｍｉｎ［ｄｉｆｆ０、ｄｉｆｆ１、・・・、ｄｉｆｆｎ−１］）を抽出する。そして、値ν０を初項、値νｎを末項、ｄｉｆｆｍｉｎを隣接項の間の差とする等差数列を生成する。この等差数列が、変数ａがとり得る値の集合と推定される。この推定された集合と、実測の集合とを比較することにより、変数ａの不連続度を特定することができる。
【００３０】
図１２は、変数ａの不連続度を特定するための別の方法を説明する概念図である。まず、抽出された条件式の中から、変数ａを含む条件式（行）を、図１２のように抽出する（条件式１５からは、変数ａを含む２つの行が抽出されている）。そして、それらの条件式（行）の中で、変数ａがどの値を取った場合に条件式が真とされるのかを判定する。この図１２の例では、変数ａの値が０、１、３のいずれかを取った場合に、抽出された行を含む条件式が真となる。一方、変数ａは、理論上は値として「２」を取ることも可能であるが、図１２に係るソースコードでは、変数ａが２の値を取ったとしても、どの条件式も真とはならず、制御が切り替わることはない。したがって、この図１２の例では、変数ａの不連続度を＃（｛０、１、２、３｝／｛０、１、３｝）＝＃｛２｝＝１と算出する。
【００３１】
［効果］
以上説明したように、第２の実施の形態のソフトウエア検証システムによれば、抽出された条件式及び変数に基づき変数の不連続度を演算し、その演算結果に基づいて状態変数を特定することができる。状態変数の特定は、人手による分析によらず自動的に、かつ的確に、しかも短時間で特定することができる。
【００３２】
［第３の実施の形態］
次に、第３の実施の形態に係るソフトウエア検証システムを、図１３〜図１６を参照して説明する。この第３の実施の形態の基本的な構成及び動作は、第１の実施の形態と同一である（図３〜図５）。ただし、この実施の形態では、上述した「非独立」の数値化を行い、その結果に基づいて状態変数を決定する。「非独立度」は、数値化部２３で数値化され、状態変数決定部２４において状態変数を決定するファクターとして用いられる。状態変数候補抽出部２１、及び条件式抽出部２２の動作は第１の実施の形態と同一である。
【００３３】
次に、変数の非独立度の具体的な計算方法の第１の例を、図１３を参照して説明する。この第１の例では、図１０において説明したのと同様に、条件式を真にする当該変数の値がどれだけ多く存在するか、という観点から変数の非独立を計算する。
【００３４】
まず、抽出された条件式の中から、１つの変数例えば変数ａを含む条件式（行）を、図１３のように抽出する（条件式１５からは、変数ａを含む２つの行が抽出されている）。そして、その各条件式（行）について、その条件式（行）が真となる変数ａの値の個数（種類）を判定する。図１３の例の場合、条件式１は、変数ａの値が１の場合にのみ真となるので、条件式１には「１」が与えられる。条件式２については、「！＝１」、すなわち、変数ａが１以外、すなわち０、２、３（３通り）の場合に条件式２が真となるので、条件式２には「３」が与えられる。
【００３５】
このようにして、すべての行について、その行の判断が真となる変数ａの値の個数を求め、その合計値を判定する。複数の条件式について、条件式を真とするような変数ａの値の個数が多ければ多いほど、変数ａは状態変数らしくない、ということができる。すなわち、この第１の例では、複数の条件式を真とするような変数ａの値の個数の合計値を求め、この合計値を非独立度Ｄ１として算出する。その他の変数ｂ〜ｅについても同様にして非独立度Ｄ１の計算を実行する。そして、状態変変数決定部２４は、変数ごとに算出された非独立度Ｄ１を比較して、変数ａ〜ｅの中から状態変数を選択する。
【００３６】
変数の非独立度の具体的な計算方法の第２の例を図１４及び図１５を参照して説明する。ここでの非独立度の概念は、第１の例の場合とは若干異なっている。一例として、図１４に示すように、変数ａを含む２つの条件式（Ｘ）、（Ｙ）があり、条件式（Ｘ）は変数ａの値が０又は１の場合に真となり、条件式（Ｙ）は変数ａの値が１又は２の場合に真となる場合を考える。
【００３７】
この場合、２つの条件式（Ｘ）と（Ｙ）はどちらも、変数ａの値が１の場合に真となり、条件式を真とする変数が重複している。このように、２つの条件式が同じ変数を含み、しかも条件式を真とする当該変数の値が重複している場合、その変数は、その重複の分だけ、少なくとも（その２つの条件式に関しては）影響度が低いということができる。
【００３８】
上記のような考え方の下、この第２の例では、図１５に示すような方法により、変数ａの非独立度Ｄ２を計算する。まず、抽出された条件式の中から、変数ａを含む条件式の行を抽出する（この図１５の例では、条件式１５から２つの行が抽出されて、合計で８つの行が抽出されている）。
そして、これらの８つの行の中から任意の２つの行を選択し、その選択された２つの行を真とする値を特定する。そして、その２つの行の両方を真とするような変数ａの値が存在するか否か、換言すれば、２つの行の両方を真とするａの値が重複しているか否かを判定する。
例えば、図１５の条件式１と条件式２を比較した場合、条件式１は変数ａが１の場合に真となり、条件式２は変数ａが２、３、又は４の場合に真となる。したがって、条件式１と条件式２との間では、両方の条件式を真とするようなａの値は存在しない（条件式を真とするような値が重複していない）。一方、条件式８と条件式９とを比較した場合、条件式８は変数ａが０又は１の場合に真となり、条件式９は変数ａが０又は３の場合に真となる。したがって、条件式８と条件式９との間では、両方の式を真とする値が存在する（重複が存在する）。以下同様にして、すべての２つの行の組み合わせ（８Ｃ２個）について同様の判定を行う。そして、条件式を真とする変数ａの値が重複している２つの条件式の組み合わせの数Ａを特定する。そして、この数αを、８つの行の任意の２つの行の組み合わせの数（全組み合わせ数（８Ｃ２個））βを特定し、非独立度Ｄ２＝α／βを求める。このＤ２の値が小さいほど、変数ａは状態変数らしいということができ、Ｄ２の値が大きいほど、変数ａは状態変数らしくないということができる。
【００３９】
変数の非独立度の具体的な計算方法の第３の例を、図１６を参照して説明する。ここでの非独立度の概念は、第１の例及び第２の例のいずれとも若干異なっている。この第３の例では、変数ａを含む複数の条件式の中で、それ単独で条件式を真にすることがない変数ａの値が存在するか否か、存在する場合にはその個数γを特定し、更に変数ａがとり得る値の個数（推定）δに対する、その個数γの割合γ／δを判定することにより、変数ａの非独立度Ｄ３を判断する。変数ａが複数の値を取り得る場合、その値のそれぞれが単独で条件式を真とするのであれば、その分だけその変数は相対的に影響度が高く、状態変数らしい変数であるということができる。一方、変数ａが複数の値を取り得るが、そのうちのいくつかの値は、それ単独で条件式を真とするのではなく、他の値の場合にも真となるのであれば、その分だけ、その変数は影響度が低いということになる。この第３の例は、上記のような観点から変数ａの非独立度Ｄ３を判断するものである。
【００４０】
例えば、変数ａを含む条件式の行が図１６に示すように抽出された場合を考える。この場合、条件式１、７、及び条件式１５（１）は、変数ａの値が１である場合にのみ真となる。また、条件式４、及び条件式１３は、変数ａの値が０である場合のみ真となる。また、条件式１５（２）は、変数ａの値が１の場合にのみ真となる。このように、変数ａは値０、１、２、３を取り得ると推定されるが、そのうち、値０、１、２の場合には、その値単独でいずれかの条件式を真にする。
【００４１】
しかし、変数ａの値が３の場合には、それ単独（ａ＝３のみ）で真となる条件式（行）が存在しない。すなわち、条件式２は、変数ａの値が３の場合に真となるが、条件式２は、変数ａの値が０又は２の場合にも真となるので、変数ａの値が３の場合にのみ、条件式２が真となるものではない。条件式９も同様である。
このように、この第３の例では、変数ａがとり得る値の個数（推定）δを特定し、更に、その値のうち、それ単独で条件式を真とすることが無い変数ａの値の数γを特定し、変数ａの非独立度Ｄ３＝γ／δを算出する。他の変数ｂ〜ｅについても同様にして非独立度Ｄ３を算出し、比較することにより状態変数を決定することができる。
【００４２】
上述したように、変数の非独立度を演算する方法は、様々なものが考えられる。上記第１の例〜第３の例で演算されるＤ１〜Ｄ３の少なくとも１つのみを採用してもよいし、上記非独立度Ｄ１〜Ｄ３を組み合わせて非独立度Ｄｍを演算してもよい。例えば、非独立度ＤｍをＤ１×（Ｄ２＋Ｄ３）として演算することができる。
【００４３】
［効果］
以上説明したように、第３の実施の形態のソフトウエア検証システムによれば、抽出された条件式及び変数に基づき変数の非独立度を演算し、その演算結果に基づいて状態変数を特定することができる。状態変数の特定は、人手による分析によらず自動的に、かつ的確に、しかも短時間で特定することができる。
【００４４】
［その他］
上述の第１〜第３の実施の形態の数値化部２３は、このような条件式中での各変数の「現れ方」を、上記のように埋没度、不連続度、又は非独立度の観点から数値化する。しかし、上述した埋没度、不連続度、及び非独立度は、変数の現れ方を表現する尺度の一例である。この３つの尺度以外の尺度を組み合わせても良いことは言うまでもなく、また、埋没度、不連続度、及び非独立度の全てを用いて状態変数を決定してもよいし、そのうちの一部を用いても良い。
例えば、埋没度、不連続度、及び独立度の全てを用いて態変数らしさを判定する場合、上述のようにして演算された埋没度、不連続度、及び非連続度の積を変数ａ〜ｅごとに演算して、この積の大小を比較することにより、状態変数を決定してもよい。
【００４５】
以上、本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【００４６】
１１・・・ＣＰＵ、  １２・・・データ入力部、  １３、１４・・・インタフェース（Ｉ／Ｏ）、  １５・・・出力装置、  １６・・・ＲＯＭ、  １７・・・ＲＡＭ、  １８・・・ハードディスクドライブ、  ２１・・・状態変数候補抽出部、  ２２・・・条件式抽出部、  ２３・・・数値化部、  ２４・・・状態変数決定部。
【図１】
2018049565.tif 000003
【図２】
2018049565.tif 000004
【図３】
2018049565.tif 000005
【図４】
2018049565.tif 000006
【図５】
2018049565.tif 000007
【図６】
2018049565.tif 000008
【図７】
2018049565.tif 000009
【図８】
2018049565.tif 000010
【図９】
2018049565.tif 000011
【図１０】
2018049565.tif 000012
【図１１】
2018049565.tif 000013
【図１２】
2018049565.tif 000014
【図１３】
2018049565.tif 000015
【図１４】
2018049565.tif 000016
【図１５】
2018049565.tif 000017
【図１６】
2018049565.tif 000018