(57)【要約】【課題】プログラムの正しさを保証する確率を高めた論理検証システムを提供する。【解決手段】論理検証システム１１は、入力値制限設定部１２と、出力値制限設定部１３と、カバレッジテスト実行部１４と、比較部１６と、出力部１７とを備える。入力値制限設定部１２は、カバレッジテストに用いる入力値の有効な制限を設定させる。出力値制限設定部１３は、カバレッジテストのテスト結果である出力値の有効な制限を設定させる。カバレッジテスト実行部１４は、プログラムに対して、入力値制限設定部１２により設定された有効な制限に従ってテスト入力値を用いて、カバレッジテストを実行する。比較部１６は、カバレッジテスト実行部１４により実行されたテスト出力値と、出力値制限設定部１３により設定された出力値の有効な制限とを比較する。出力部１７は、コードカバレッジ測定部１５による測定結果、および比較部１６による比較結果を出力する。【選択図】図１
2017117216.tif 000002
【特許請求の範囲】
【請求項１】
コンピューターによる情報処理を用いて、カバレッジテストを行ってプログラムの論理検証を行う論理検証システムであって、
前記カバレッジテストに用いる入力値の有効な制限を設定させる入力値制限設定部と、
前記カバレッジテストのテスト結果である出力値の有効な制限を設定させる出力値制限設定部と、
前記プログラムに対して、前記入力値制限設定部により設定された有効な制限に従ってテスト入力値を用いて、前記カバレッジテストを実行するカバレッジテスト実行部と、
前記カバレッジテスト実行部により実行されたテスト結果から、前記プログラムのコードカバレッジを測定するコードカバレッジ測定部と、
前記カバレッジテスト実行部により実行されたテスト出力値と、前記出力値制限設定部により設定された前記出力値の有効な制限とを比較する比較部と、
前記コードカバレッジ測定部による測定結果、および前記比較部による比較結果を出力する出力部とを備える、論理検証システム。
【請求項２】
前記入力値制限設定部により設定された制限に基づいて、前記カバレッジテストのテスト入力値を生成するテスト入力値生成部をさらに備え、
前記カバレッジテスト実行部は、前記テスト入力値生成部により生成された前記テスト入力値を用いて、前記カバレッジテストを実行する、請求項１に記載の論理検証システム。
【請求項３】
前記入力値制限設定部は、前記入力値の上限値、前記入力値の下限値、および前記入力値同士の間隔を規定する刻み値のうちの少なくともいずれか一方を設定させる、請求項１または２に記載の論理検証システム。
【請求項４】
前記出力値制限設定部は、前記出力値の上限値、前記出力値の下限値、および前記出力値同士の間隔を規定する刻み値のうちの少なくともいずれか一方を設定させる、請求項１〜３のいずれか１項に記載の論理検証システム。
【請求項５】
前記入力値制限設定部は、前記カバレッジテストの入力値を記載した入力値ファイルを読み込むことにより、前記入力値の有効な制限を設定させる、請求項１〜４のいずれか１項に記載の論理検証システム。
【請求項６】
前記出力値制限設定部は、前記カバレッジテストのテスト出力値を記載した出力値ファイルを読み込むことにより、前記出力値の有効な制限を設定させ、
前記比較部は、前記カバレッジテスト実行部により実行されたテスト結果と、前記出力値制限設定部により読み込まれた前記出力値ファイルとを比較する、請求項１〜５のいずれか１項に記載の論理検証システム。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、論理検証システムに関するものである。
【背景技術】
【０００２】
例えば、画像形成装置といった電子機器を作動させて何らかの処理を行う上においては、複数のソフトウェアが実行される。ソフトウェアの実行に先立って、ソフトウェアを構成するプログラムを記述したソースコードが適切か否かを、テストデータを用いたテストによって検証する場合がある。ソフトウェアの論理検証に関する技術が、特開２００６−８５６５８号公報（特許文献１）、および特開２００５−１４１６１６号公報（特許文献２）に開示されている。
【０００３】
特許文献１によると、論理検証システムは、乱数テストデータ生成部と、ソフトウェアカバレッジ情報出力部と、ハードウェアカバレッジ情報出力部とを備える構成である。そして、論理検証実行時のカバレッジ出力情報の変化から、テストデータの有効性を評価し、有効なテストデータのみを選別して蓄積している。また、テスト再実行時は、有効なテストデータのみ再実行することにより検証効率を向上し、論理検証期間を短縮することとしている。
【０００４】
特許文献２によると、論理検証システムは、乱数テストデータ生成部と、論理シミュレータと、カバレッジ判定部と、追加テスト条件生成判定部とを有する構成である。乱数テストデータ生成部は、テスト条件情報に基づき乱数テストデータを生成する処理を行う。論理シミュレータは、乱数テストデータを入力データとして対象論理の論理シミュレーション処理を実行しカバレッジ情報を出力する。カバレッジ判定部は、カバレッジ情報の出力と、カバレッジの網羅率を示すカバレッジ蓄積情報とを用いて、テスト時のカバレッジの変化の判定処理を行い、カバレッジが向上した部分に対応する乱数テストデータまたはそのテスト条件情報をテスト条件蓄積情報として蓄積する処理を行う。追加テスト条件生成判定部は、カバレッジ蓄積情報とテスト条件蓄積情報とをもとに作成されたテスト条件生成判定情報を用いて、追加テスト条件を生成するか判定処理し、その結果、追加テスト条件情報を生成して格納する処理を行う。また、追加テスト条件生成判定部は、テスト条件生成判定情報を参照し、前回のテスト時のカバレッジ情報と、今回のテスト時のカバレッジ情報とを比較し、前回のテスト時にはカバーできていたが今回のテスト時にはカバーできていないテストケースを抜き出し、追加テスト条件として生成する処理を行う。そして、乱数テストデータ生成部により、追加テスト条件を用いたテストを可能としている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２０１０−１４６０３７号公報
【特許文献２】特開２０１３−２００６６２号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
プログラムを検証する論理検証システムにおいて、プログラムの検証の際に用いられるカバレッジテストは、いわゆる実行網羅率を定量的に測定するものである。
【０００７】
ここで、カバレッジテストの結果について、その値が高いということは、プログラムを構成するコードのテストによる網羅率が高いということである。しかし、網羅率が高い場合であっても、必ずしもプログラムの正しさを保証する確率が高くなる訳ではない。
【０００８】
例えば、実際にはプログラムとしてあり得ないような入力値が入力され、テスト結果においてプログラムの網羅率が高い結果が得られても、実質的に意味のないテストとなってしまう。出力値についても、同様である。
【０００９】
具体的には、除算の関数を含むプログラムについて考えると、以下のようになる。カバレッジテストにおいて用いられる入力値は、ランダムなデータが用いられる。ここで、割る数として「０」以外の入力値がランダムに選択された場合には、割る数として「０」が入力された場合を異常動作として検出するコードが記述されていなくとも、正常な処理が行われることとなる。そして、この場合、網羅率は１００％となる。
【００１０】
しかし、割る数として「０」が入力値に選択された場合に、異常動作として検出するコードが記述されていなければ、プログラムは適切な処理を行うことができない。そうすると、このような場合にプログラムの不具合を検出することができないこととなる。その結果、プログラムの正しさを保証できないことになる。
【００１１】
特許文献１においては、論理検証実行時のカバレッジ出力情報の変化から、テストデータの有効性を評価し、有効なテストデータのみを選別して蓄積し、テスト再実行時は、有効なテストデータのみ再実行することとしている。また、特許文献２においては、カバレッジ蓄積情報とテスト条件蓄積情報とをもとに作成されたテスト条件生成判定情報を用いて、追加テスト条件を生成するか判定処理し、その結果、追加テスト条件情報を生成して格納する処理を行う追加テスト条件生成判定部を有することとしている。しかし、これらのような技術では、上記した問題を解消することが困難である。
【００１２】
この発明の目的は、プログラムの正しさを保証する確率を高めた論理検証システムを提供することである。
【課題を解決するための手段】
【００１３】
この発明の論理検証システムは、コンピューターによる情報処理を用いて、カバレッジテストを行ってプログラムの論理検証を行う。論理検証システムは、入力値制限設定部と、出力値制限設定部と、カバレッジテスト実行部と、コードカバレッジ測定部と、比較部と、出力部とを備える。入力値制限設定部は、カバレッジテストに用いる入力値の有効な制限を設定させる。出力値制限設定部は、カバレッジテストのテスト結果である出力値の有効な制限を設定させる。カバレッジテスト実行部は、プログラムに対して、入力値制限設定部により設定された有効な制限に従ってテスト入力値を用いて、カバレッジテストを実行する。コードカバレッジ測定部は、カバレッジテスト実行部により実行されたテスト結果から、プログラムのコードカバレッジを測定する。比較部は、カバレッジテスト実行部により実行されたテスト出力値と、出力値制限設定部により設定された出力値の有効な制限とを比較する。出力部は、コードカバレッジ測定部による測定結果、および比較部による比較結果を出力する。
【発明の効果】
【００１４】
このような論理検証システムによれば、入力値制限設定部により、入力値の有効な制限を設定させているため、カバレッジテストを実行する際の入力値において、プログラムとしてあり得ないようなデータが入力されることはない。この場合、入力値の数を制限して、テストパターンの数を減らし、効率的にカバレッジテストを実行することができる。また、出力値制限設定部により、出力値の有効な制限を設定させているため、カバレッジテストを実行した際の出力値において、設定された有効な制限との比較を行うことができる。そうすると、この比較結果とカバレッジテストのテスト結果に基づき、プログラムの正しさを判断することができる。したがって、このような論理検証システムは、プログラムの正しさを保証する確率を高めることができる。
【図面の簡単な説明】
【００１５】
【図１】この発明の一実施形態に係る論理検証システムの構成を示すブロック図である。
【図２】図１に示す論理検証システムを用いて、プログラムＰのカバレッジテストを実行する場合の処理の流れを示すフローチャートである。
【図３】１回の処理で有効な制限として設定された入力値ファイルと出力値ファイルの内容を示す図である。
【図４】この発明の他の実施形態に係る論理検証システムの構成を示すブロック図である。
【図５】図４に示す論理検証システムを用いて、プログラムＱのカバレッジテストを実行する場合の処理の流れを示すフローチャートである。
【図６】有効な制限として設定された入力値ファイルと出力値ファイルの内容を示す図である。
【図７】テスト入力値が生成される状態を示す図である。
【図８】テスト出力値の状態を示す図である。
【発明を実施するための形態】
【００１６】
以下、この発明の実施の形態を説明する。図１は、この発明の一実施形態に係る論理検証システム１１の構成を示すブロック図である。なお、図１中の矢印は、制御信号や制御、データの流れを示している。
【００１７】
図１を参照して、論理検証システム１１は、ハードウェアとしてのコンピューターによる情報処理を用いて、プログラムの論理検証を行う。論理検証システム１１は、入力値制限設定部１２と、出力値制限設定部１３と、カバレッジテスト実行部１４と、コードカバレッジ測定部１５と、比較部１６と、出力部１７とを備える。入力値制限設定部１２は、カバレッジテストに用いる入力値の有効な制限を設定させる。出力値制限設定部１３は、カバレッジテストのテスト結果である出力値の有効な制限を設定させる。カバレッジテスト実行部１４は、プログラムに対して、入力値制限設定部１２により設定された有効な制限に従ってテスト入力値を用いて、カバレッジテストを実行する。コードカバレッジ測定部１５は、カバレッジテスト実行部１４により実行されたテスト結果から、プログラムのコードカバレッジを測定する。比較部１６は、カバレッジテスト実行部１４により実行されたテスト出力値と、出力値制限設定部１３により設定された出力値の有効な制限とを比較する。出力部１７は、コードカバレッジ測定部１５による測定結果、および比較部１６による比較結果を出力する。
【００１８】
また、入力値制限設定部１２は、カバレッジテストの入力値を記載した入力値ファイルを読み込むことにより、入力値の有効な制限を設定させる。出力値制限設定部１３は、カバレッジテストのテスト出力値を記載した出力値ファイルを読み込むことにより、出力値の有効な制限を設定させる。比較部１６は、カバレッジテスト実行部１４により実行されたテスト結果と、出力値制限設定部１３により読み込まれた出力値ファイルとを比較する。
【００１９】
次に、このような構成の論理検証システム１１を用いて、プログラムＰのカバレッジテストを行う場合について説明する。図２は、図１に示す論理検証システム１１を用いて、プログラムＰのカバレッジテストを実行する場合の処理の流れを示すフローチャートである。ここで、プログラムＰは、自動販売機における入金と商品を購入した際の釣銭との関係を示すプログラムＰである。
【００２０】
図１および図２を参照して、まず、入力値、および出力値について、入力値制限設定部１２、および出力値制限設定部１３はそれぞれ、有効な制限を設定させる（図２において、ステップＳ１１、以下、「ステップ」を省略する）。入力値、および出力値のそれぞれについて、それぞれ個別に設定させる。この場合、カバレッジテストの入力値を記載した入力値ファイル、およびカバレッジテストのテスト出力値を記載した出力値ファイルをそれぞれ読み取らせることにより、有効な制限を設定させる。
【００２１】
図３は、１回の処理で有効な制限として設定された入力値ファイル２１ａと出力値ファイル２１ｂ、すなわち、出力値として期待される数値のファイルの内容を示す図である。図３を参照して、入力値ファイル２１ａには、１回の入金時の処理として１０円玉硬貨が投入された際の処理に相当する１０という入力値、同じく５０、１００、５００、そして、１０００円札が投入された際の処理に相当する１０００という入力値、同じく２０００、５０００、１００００という８つのテスト入力値がある。すなわち、入力値として、上記した８つの入力値という有効な制限が設定されている。
【００２２】
また、出力値ファイル２１ｂには、１回の釣銭の出力の処理として、１０円玉硬貨をお釣りとして排出する際の処理に相当する１０という出力値、同じく５０、１００、５００、そして、１０００円札を釣銭として排出する際の処理に相当する１０００、同じく２０００、５０００という７つのテスト出力値がある。すなわち、出力値として、上記した７つの出力値という有効な制限が設定されている。
【００２３】
入力値制限設定部１２、および出力値制限設定部１３においてこれらの入力値、および出力値が設定されると、カバレッジテスト実行部１４は、設定された有効な制限に従ってテスト入力値を用いて、カバレッジテストを実行する（Ｓ１２）。この場合、入力値として、全ての値、具体的には、８つのテスト入力値についてカバレッジテストを実行する。
【００２４】
次に、カバレッジテスト実行部１４により実行されたテスト結果から、コードカバレッジ測定部１５により、コードカバレッジが測定される（Ｓ１３）。また、ここで、比較部１６は、カバレッジテスト実行部１４により実行されたテスト出力値１８と、出力値制限設定部１３により設定された出力値の有効な制限とを比較する（Ｓ１４）。この場合、比較部１６は、カバレッジテスト実行部１４により実行されたテスト結果と、出力値制限設定部１３により読み込まれた出力値ファイルとを比較する。具体的には、カバレッジテスト実行部１４により実行されたテスト出力値１８が、出力値ファイル２１ｂに記載された７つのテスト出力値のいずれかに相当するか否かを比較する。
【００２５】
その後、出力部１７は、コードカバレッジ測定部１５による測定結果、および比較部１６による比較結果を出力する（Ｓ１５）。すなわち、コードカバレッジ測定部１５により測定されたコードカバレッジ結果、および出力値ファイル２１ｂに記載された７つのテスト出力値のいずれかに相当したか否かの結果が出力される。
【００２６】
このような構成の論理検証システム１１によれば、入力値制限設定部１２により、入力値の有効な制限を設定させているため、カバレッジテストを実行する際の入力値において、プログラムとしてあり得ないようなデータが入力されることはない。この場合、入力値の数を制限して、テストパターンの数を減らし、効率的にカバレッジテストを実行することができる。また、出力値制限設定部１３により、出力値の有効な制限を設定させているため、カバレッジテストを実行した際の出力値において、設定された有効な制限との比較を行うことができる。そうすると、この比較結果とカバレッジテストのテスト結果に基づき、プログラムの正しさを判断することができる。したがって、このような論理検証システム１１は、プログラムの正しさを保証する確率を高めることができる。
【００２７】
この場合、入力値および出力値は、ファイルで読み取られるため、入力値の制限の設定、および出力値の制限の設定をより簡易的に行うことができる。
【００２８】
なお、上記の実施の形態において、１回の処理として、硬貨に限定されるようなプログラムの場合、１０、５０、１００、５００という４つのテスト入力値２２ａ、および１０、５０、１００、５００という４つのテスト出力値２２ｂに限定される。
【００２９】
なお、論理検証システム１１は、入力値制限設定部１２により設定された制限に基づいて、カバレッジテストのテスト入力値を生成するテスト入力値生成部をさらに備える構成としてもよい。また、カバレッジテスト実行部１４は、テスト入力値生成部により生成されたテスト入力値を用いて、カバレッジテストを実行するようにしてもよい。また、入力値制限設定部１２は、入力値の上限値、および入力値の下限値を設定させるよう構成してもよい。また、出力値制限設定部１３は、出力値の上限値、および出力値の下限値を設定させるよう構成してもよい。
【００３０】
図４は、この発明の他の実施形態に係る論理検証システム２６の構成を示すブロック図である。図４において、図１と同様の構成の部材については、同一の符号を付して、それらの説明を省略する。
【００３１】
図４を参照して、論理検証システム２６は、入力値制限設定部１２と、出力値制限設定部１３と、テスト入力値生成部２７と、カバレッジテスト実行部１４と、コードカバレッジ測定部１５と、比較部１６と、出力部１７とを備える。テスト入力値生成部２７は、入力値制限設定部１２により設定された制限に基づいて、テストデータ２８からカバレッジテストのテスト入力値を生成する。
【００３２】
次に、このような構成の論理検証システム２６を用いて、プログラムＱのカバレッジテストを行う場合について説明する。図５は、図４に示す論理検証システム２６を用いて、プログラムＱのカバレッジテストを実行する場合の処理の流れを示すフローチャートである。ここで、プログラムＱは、ある地点における気圧のデータからその地点の高度を算出するプログラムＱである。
【００３３】
図５を参照して、入力値、および出力値について、入力値制限設定部１２、および出力値制限設定部１３はそれぞれ、有効な制限を設定させる（Ｓ２１）。ここで、入力値制限設定部１２は、入力値の上限値、および入力値の下限値の双方を設定させる。また、出力値制限設定部１３は、出力値の上限値、および出力値の下限値をそれぞれ設定させる。
【００３４】
図６は、有効な制限として設定された入力値ファイル３１ａと出力値ファイル３１ｂ、すなわち、出力値として期待される数値のファイルの内容を示す図である。図６を参照して、入力値ファイル３１ａの下限値として、「ｘｘｘｘ」という値、入力ファイル３１ａの上限値として、「ｙｙｙｙ」という値が設定される。また、出力ファイル３１ｂの下限値としては、「０」という値、出力ファイル３１ｂの上限値としては、「８８４８」という値が設定される。出力ファイル３１ｂの下限値としては、海抜０ｍ（メートル）が設定されており、出力ファイル３１ｂの上限値としては、地上における最高峰であるエベレストの山頂の高度である８８４８（ｍ）が入力されている。すなわち、８８４８（ｍ）以上の高度が算出されれば、この地球上のどの場所においてもそのような場所は存在しないため、エラーとして算出すべきものとされる。
【００３５】
次に、テスト入力値生成部２７は、複数の数値群から構成されるテストデータ２８を基に、テスト入力値２９を生成する（Ｓ２２）。図７は、テスト入力値３３ａが生成される状態を示す図である。図７を参照して、下限値を「ｘｘｘｘ」とし、上限値を「ｙｙｙｙ」とする数値群３２ａの中から、一つのテスト入力値３３ａをランダムに抽出して生成する。
【００３６】
なお、ここで、従来におけるテスト入力値の生成について説明する。図７において、一点鎖線より上部の領域が、従来の場合である。従来の場合、下限値は「ｘｘｘｘ」よりも小さい「ｚｚｚｚ」という値であり、上限値は「ｙｙｙｙ」よりも大きい「ｗｗｗｗ」という値である。この「ｘｘｘｘ」よりも小さく「ｚｚｚｚ」よりも大きい値、および「ｙｙｙｙ」よりも大きく「ｗｗｗｗ」よりも小さい値については、プログラムＱにおいて、入力値としてあり得ないものである。そして、従来において、「ｚｚｚｚ」よりも大きく「ｗｗｗｗ」よりも小さい数値群３２ｂの中からランダムに選択されるテスト入力値３３ｂについては、「ｘｘｘｘ」よりも小さく「ｚｚｚｚ」よりも大きい値が選択される場合がある。
【００３７】
入力値制限設定部１２、および出力値制限設定部１３においてこれらの入力値、および出力値が設定されると、カバレッジテスト実行部１４は、生成されたテスト入力値３３ａを用いて、プログラムＱに対して、カバレッジテストを実行する（Ｓ２３）。
【００３８】
次に、カバレッジテスト実行部１４により実行されたテスト結果から、コードカバレッジ測定部１５により、コードカバレッジが測定される（Ｓ２４）。また、ここで、比較部１６は、カバレッジテスト実行部１４により実行されたテスト出力値１８と、出力値制限設定部１３により設定された出力値の有効な制限とを比較する（Ｓ２５）。この場合、比較部１６は、カバレッジテスト実行部１４により実行されたテスト結果と、出力値制限設定部１３により読み込まれた出力値ファイルとを比較する。
【００３９】
図８は、テスト出力値の状態を示す図である。図８を参照して、テスト出力値３４ａと、設定された上限値および下限値とを比較する。具体的には、下限値を「０」とし、上限値を「８８４８」とする数値群３５ａの中に、テスト出力値３４ａが含まれているか否かを比較して判断する。この場合、テスト出力値３４ａは、数値群３５ａの中に含まれているため、適切なプログラムＱによる処理、すなわち、気圧の値から高度の算出の処理が適切になされていることが把握できる。
【００４０】
なお、ここで、従来におけるテスト出力値の生成について説明する。図８において、一点鎖線より上部の領域が、従来の場合である。従来の場合、下限値は「０」よりも小さい「ｖｖｖｖ」という値であり、上限値は「８８４８」よりも大きい「ｕｕｕｕ」という値である。この「０」よりも小さく「ｖｖｖｖ」よりも大きい値、および「８８４８」よりも大きく「ｕｕｕｕ」よりも小さい値については、プログラムＱによる処理において、出力値としてあり得ないものである。そして、従来において、「ｖｖｖｖ」よりも大きく「ｕｕｕｕ」よりも小さい数値群３５ｂの中に含まれるテスト出力値３４ｂについては、「０」よりも小さく「ｖｖｖｖ」よりも大きい値が出力される場合がある。このような場合は、プログラムＱによる適切な処理がなされておらず、プログラムＱに不具合が含まれていることが把握できる。
【００４１】
その後、出力部１７は、コードカバレッジ測定部１５による測定結果、および比較部１６による比較結果を出力する（Ｓ２６）。すなわち、コードカバレッジ測定部１５により測定されたコードカバレッジ結果、および設定された出力値の下限値と上限値の間にテスト出力値３４ａが含まれているかの結果が出力される。
【００４２】
このような構成の論理検証システム２６は、よりプログラムの正しさを保証する確率を高めることができる。
【００４３】
この場合、テスト入力値生成部２７によりテスト入力値を生成することとしているため、より簡易的にテスト入力値を生成することができる。
【００４４】
なお、上記の実施の形態において、下限値を「ｘｘｘｘ」とし、上限値を「ｙｙｙｙ」とする数値群３２ａにおける全てのテスト入力値３３ａを用いて、テストを行ってもよい。下限値を「ｘｘｘｘ」とし、上限値を「ｙｙｙｙ」とする数値群３２ａにおける全てのテスト入力値３３ａを用いてテストを行う際に、エラーが発生すれば、その時点で処理を終了することにしてもよい。
【００４５】
なお、上記の実施の形態においては、入力値制限設定部１２は、入力値の上限値、および入力値の下限値の双方を設定させることとしたが、これに限らず、入力値制限設定部１２は、入力値の上限値、入力値の下限値、および入力値同士の間隔を規定する刻み値のうちの少なくともいずれか一方を設定させるよう構成してもよい。
【００４６】
また、上記の実施の形態においては、出力値制限設定部１３は、出力値の上限値、および出力値の下限値をそれぞれ設定させることとしたが、これに限らず、出力値制限設定部１３は、出力値の上限値、出力値の下限値、および出力値同士の間隔を規定する刻み値のうちの少なくともいずれか一方を設定させるよう構成してもよい。
【００４７】
今回開示された実施の形態はすべての点で例示であって、どのような面からも制限的なものではないと理解されるべきである。本発明の範囲は上記した説明ではなく、特許請求の範囲によって規定され、特許請求の範囲と均等の意味および範囲内でのすべての変更が含まれることが意図される。
【産業上の利用可能性】
【００４８】
この発明に係る論理検証システムは、プログラムの正しさを保証する確率の向上が要求される場合に、特に有効に利用される。
【符号の説明】
【００４９】
１１，２６  論理検証システム、１２  入力値制限設定部、１３  出力値制限設定部、１４  カバレッジテスト実行部、１５  コードカバレッジ測定部、１６  比較部、１７  出力部、１８，２２ｂ，３３ａ，３３ｂ，３４ａ，３４ｂ  テスト出力値、２１ａ，３１ａ  入力値ファイル、２１ｂ，３１ｂ  出力値ファイル、２２ａ，２９  テスト入力値、２７  テスト入力値生成部、２８  テストデータ、３２ａ，３２ｂ，３５ａ，３５ｂ  数値群。
【図１】
2017117216.tif 000003
【図２】
2017117216.tif 000004
【図３】
2017117216.tif 000005
【図４】
2017117216.tif 000006
【図５】
2017117216.tif 000007
【図６】
2017117216.tif 000008
【図７】
2017117216.tif 000009
【図８】
2017117216.tif 000010
【手続補正書】
【提出日】平成27年12月25日(2015.12.25)
【手続補正１】
【補正対象書類名】明細書
【補正対象項目名】０００２
【補正方法】変更
【補正の内容】
【０００２】
例えば、画像形成装置といった電子機器を作動させて何らかの処理を行う上においては、複数のソフトウェアが実行される。ソフトウェアの実行に先立って、ソフトウェアを構成するプログラムを記述したソースコードが適切か否かを、テストデータを用いたテストによって検証する場合がある。ソフトウェアの論理検証に関する技術が、特開２０１０−１４６０３７号公報（特許文献１）、および特開２０１３−２００６６２号公報（特許文献２）に開示されている。
【手続補正２】
【補正対象書類名】明細書
【補正対象項目名】００４９
【補正方法】変更
【補正の内容】
【００４９】
１１，２６  論理検証システム、１２  入力値制限設定部、１３  出力値制限設定部、１４  カバレッジテスト実行部、１５  コードカバレッジ測定部、１６  比較部、１７  出力部、１８，２２ｂ，３４ａ，３４ｂ  テスト出力値、２１ａ，３１ａ  入力値ファイル、２１ｂ，３１ｂ  出力値ファイル、２２ａ，２９，３３ａ，３３ｂ  テスト入力値、２７  テスト入力値生成部、２８  テストデータ、３２ａ，３２ｂ，３５ａ，３５ｂ  数値群。