(57)【要約】      （修正有）【課題】より効率的にプログラムの仕様に対する一致性検証を行うことが可能な技術を提供する。【解決手段】情報処理装置は、検証対象のプログラム３１０の入力から出力までの条件分岐経路の全パターン、及び該条件分岐経路の全パターンのそれぞれに対応する出力演算値により構成されるカットセット表３１１が、検証対象のプログラムのベースとなる仕様モデル３００のカットセット表３０１と整合しているか否かを判定する第１の整合性判定部と、仕様モデルのカットセットが、プログラムのカットセットと整合しているか否かを判定する第２の整合性判定部と、第１の整合性判定部及び第２の整合性判定部の判定結果に基づき、プログラムが仕様モデルと一致しているか否かを検証する検証部と、を備える。【選択図】図３
2019197329.tif 000002
【特許請求の範囲】
【請求項１】
検証対象のプログラムの入力から出力までの条件分岐経路の全パターン、及び、該条件分岐経路の全パターンのそれぞれに対応する出力演算値により構成されるカットセットが、検証対象のプログラムのベースとなる仕様モデルの前記カットセットと整合しているか否かを判定する第１の整合性判定部と、
前記仕様モデルの前記カットセットが、前記プログラムの前記カットセットと整合しているか否かを判定する第２の整合性判定部と、
前記第１の整合性判定部及び前記第２の整合性判定部の判定結果に基づき、前記プログラムが前記仕様モデルと一致しているか否かを検証する検証部と、を備える、
情報処理装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報処理装置に関する。
【背景技術】
【０００２】
例えば、検証対象のプログラムから生成した抽象構文木を、検証プログラムに対応する内部仕様の抽象構文木と比較することにより、該プログラムが内部仕様を満足しているかを検証する技術が知られている（例えば、特許文献１等参照）。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２０１１−２１５９９８号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、上述の技術の場合、仕様と同一の結果が得られ、十分に仕様を満足するプログラムであっても、仕様を実現する構成要素（変数名、定数名、演算方法、処理順序等）が変更されていると、仕様を満足していると判断されない可能性がある。そのため、内部仕様の検討段階で、構成要素の作り込みが求められ、結果として、プログラムの仕様に対する一致性検証に要する時間が増大してしまう可能性がある。
【０００５】
そこで、上記課題に鑑み、より効率的にプログラムの仕様に対する一致性検証を行うことが可能な技術を提供することを目的とする。
【課題を解決するための手段】
【０００６】
上記目的を達成するため、本発明の一実施形態では、
検証対象のプログラムの入力から出力までの条件分岐経路の全パターン、及び、該条件分岐経路の全パターンのそれぞれに対応する出力演算値により構成されるカットセットが、検証対象のプログラムのベースとなる仕様モデルの前記カットセットと整合しているか否かを判定する第１の整合性判定部と、
前記仕様モデルの前記カットセットが、前記プログラムの前記カットセットと整合しているか否かを判定する第２の整合性判定部と、
前記第１の整合性判定部及び前記第２の整合性判定部の判定結果に基づき、前記プログラムが前記仕様モデルと一致しているか否かを検証する検証部と、を備える、
情報処理装置が提供される。
【０００７】
本実施形態によれば、情報処理装置は、仕様モデル及びプログラムのそれぞれの、条件分岐経路の全パターン及び条件分岐経路の全パターンのそれぞれに対応する出力演算値（出力結果）により構成されるカットセットの間の整合性に基づき、一致性を検証する。そのため、情報処理装置は、仕様を実現するための具体的な構成要素の内容に依らず、プログラムの仕様に対する一致性検証を実行できる。従って、情報処理装置は、より効率的にプログラムの仕様に対する一致性検証を行うことができる。
【発明の効果】
【０００８】
本実施形態によれば、より効率的にプログラムの仕様に対する一致性検証を行うことが可能な技術を提供することができる。
【図面の簡単な説明】
【０００９】
【図１】情報処理装置の一例を示すハードウェアによる構成図である。
【図２】情報処理装置の一例を示す機能ブロック図である。
【図３】情報処理装置による一致性検証処理の一例を示すフロー図である。
【図４】カットセット表の一例を説明する図である。
【図５】カットセット表の生成対象の仕様モデル及び検証対象プログラムの一例を説明する図である。
【図６】プログラムスライシングの実行結果の一例を説明する図である。
【図７】依存グラフの一例を説明する図である。
【図８】一階述語論理式の一例について説明する図である。
【図９】ＤＮＦの論理式の一例について説明する図である。
【図１０】分割された最小項の一例について説明する図である。
【図１１】仕様モデルから見た検証対象プログラムの条件分岐経路の整合性判定処理の一例を示すフロー図である。
【図１２】検証対象プログラムの条件分岐経路の全パターンの中から仕様モデルの条件分岐経路に対応する条件分岐経路を抽出する方法の一例を説明する図である。
【図１３】仕様モデルから見た検証対象プログラムの条件分岐経路と出力結果との組み合わせの整合性判定処理の一例を示すフロー図である。
【図１４】検証対象プログラムから見た仕様モデルの条件分岐経路の整合性判定処理の一例を示すフロー図である。
【図１５】仕様モデルの条件分岐経路の全パターンの中から検証対象プログラムの条件分岐経路に対応するに条件分岐経路を抽出する方法の一例を説明する図である。
【図１６】検証対象プログラムから見た仕様モデルの条件分岐経路と出力結果との組み合わせの整合性判定処理の一例を示すフロー図である。
【図１７】仕様モデルと検証対象プログラムの一致性検証の方法を説明する図である。
【発明を実施するための形態】
【００１０】
以下、図面を参照して発明を実施するための形態について説明する。
【００１１】
［情報処理装置のハードウェア構成］
まず、図１を参照して、情報処理装置１０のハードウェアによる構成について説明する。
【００１２】
図１は、本実施形態に係る情報処理装置の一例（情報処理装置１０）を示すハードウェアによる構成図である。
【００１３】
情報処理装置１０は、ドライブ装置１００と、補助記憶装置１０２と、メモリ装置１０３と、ＣＰＵ１０４と、インタフェース装置１０５と、表示装置１０６と、入力装置１０７を含み、それぞれがバスＢで接続される。
【００１４】
情報処理装置１０での処理を実現するプログラム（以下、便宜的に「処理プログラム」）は、記録媒体１０１によって提供される。記録媒体１０１は、例えば、ＣＤ−ＲＯＭ（Compact Disc Read Only Memory）、ＤＶＤ−ＲＯＭ（Digital Versatile Disc Read Only Memory）、或いは、ＵＳＢ（Universal Serial Bus）メモリ等の可搬型の記録媒体である。記録媒体１０１及び補助記憶装置１０２のいずれについても、コンピュータ読み取り可能な記録媒体に相当する。処理プログラムが記録された記録媒体１０１が、ドライブ装置１００にセットされると、処理プログラムが記録媒体１０１からドライブ装置１００を介して補助記憶装置１０２にインストールされる。また、処理プログラムは、インターネットやローカルネットワーク等の所定のネットワークを介して他のコンピュータからダウンロードされ、補助記憶装置１０２にインストールされてもよい。
【００１５】
補助記憶装置１０２は、インストールされた処理プログラムを格納すると共に、必要なファイルやデータ等を格納する。補助記憶装置１０２は、例えば、ＨＤＤ（Hard Disk Drive）、フラッシュメモリ等である。
【００１６】
メモリ装置１０３は、処理プログラムの起動指示があった場合に、補助記憶装置１０２から処理プログラムを読み出して格納する。
【００１７】
ＣＰＵ１０４は、メモリ装置１０３に格納された処理プログラムを実行し、処理プログラムに従って情報処理装置１０に係る各種機能を実現する。
【００１８】
インタフェース装置１０５は、例えば、ネットワークに接続するためのインタフェースとして用いられる。
【００１９】
表示装置１０６は、処理プログラムによるＧＵＩ（Graphical User Interface）等を表示する。
【００２０】
入力装置１０７は、例えば、キーボード、マウス、タッチパネル、ボタン等を含み、情報処理装置１０に関する様々な操作指示をユーザに入力させるために用いられる。
【００２１】
［情報処理装置の機能構成］
次に、図２を参照し、情報処理装置１０の機能構成について説明する。
【００２２】
図２は、本実施形態に係る情報処理装置の一例（情報処理装置１０）を示す機能ブロック図である。
【００２３】
情報処理装置１０は、補助記憶装置１０２にインストールされる一以上の処理プログラムをＣＰＵ１０４に実行させることにより実現される機能部として、取得部１１、カットセット表生成部１２と、一致性検証部１３を含む。
【００２４】
取得部１１は、例えば、所定の制御対象を制御するために制御装置に実装（インストール）される予定の検証対象のプログラム（以下、便宜的に「検証対象プログラム」）を取得する。また、取得部１１は、検証対象プログラムのベースである仕様（例えば、ロジックモデル。以下、「仕様モデル」）を取得する。仕様モデルは、制御仕様が抽象的に記述された所定の形式のデータである。
【００２５】
カットセット表生成部１２は、仕様モデル及び検証対象プログラムのそれぞれについて、入力から出力までの条件分岐経路の全パターンと、当該条件分岐経路の全パターンに対応する出力演算値（出力結果）とにより構成される表形式のカットセット（以下、「カットセット表」）を生成する。カットセット表の内容及び生成方法等の詳細は、後述する（図４〜図１０参照）。
【００２６】
一致性検証部１３は、検証対象プログラムの仕様（仕様モデル）に対する一致性を検証する。一致性検証部１３は、入出力整合性判定部１３１と、トップダウン経路整合性判定部１３２と、トップダウン全体整合性判定部１３３と、ボトムアップ経路整合性判定部１３４と、ボトムアップ全体整合性判定部１３５と、検証部１３６を含む。
【００２７】
入出力整合性判定部１３１は、仕様モデルと検証対象プログラムのそれぞれの入力情報及び出力情報を比較し、仕様モデル及び検証対象プログラムの間の入出力の整合性を判定する。具体的には、入出力整合性判定部１３１は、仕様モデルで規定される入力情報及び出力情報に対して、検証対象プログラムに対応する入力情報及び出力情報が過不足なく存在するか否かを判定する。このとき、入出力整合性判定部１３１は、仕様モデルの入力情報及び出力情報と、検証対象プログラムの入力情報及び出力情報との対応関係を示すデータ（以下、「入出力対応関係データ」）を出力してよい。これにより、情報処理装置１０は、検証対象プログラムにおいて、定数名、変数名、処理順等が仕様モデルから変更されている場合でも、後述のカットセット表に基づく処理を適切に実行できる。
【００２８】
トップダウン経路整合性判定部１３２は、カットセット表に基づき、検証対象プログラムの条件分岐経路の全パターンが、仕様モデルの条件分岐経路の全パターンと整合しているか否かを判定する。つまり、トップダウン経路整合性判定部１３２は、仕様モデル側からのトップダウンアプローチで、仕様モデル及び検証対象プログラムの間の条件分岐経路の整合性を判定する。詳細は、後述する（図１１、図１２参照）。
【００２９】
トップダウン全体整合性判定部１３３（第１の整合性判定部の一例）は、カットセット表に基づき、検証対象プログラムの条件分岐経路と出力演算値との組み合わせの全パターンが、仕様モデルの条件分岐経路と出力演算値との組み合わせの全パターンに対して、整合しているか否かを判定する。つまり、トップダウン全体整合性判定部１３３は、仕様モデル側からのトップダウンアプローチで、仕様モデル及び検証対象プログラムの間の条件分岐経路と出力演算値との組み合わせの整合性（全体整合性）を判定する。詳細は、後述する（図１３参照）。
【００３０】
ボトムアップ経路整合性判定部１３４は、カットセット表に基づき、仕様モデルの条件分岐経路の全パターンが、検証対象プログラムの条件分岐経路の全パターンと整合しているか否かを判定する。つまり、ボトムアップ経路整合性判定部１３４は、検証対象プログラム側からのボトムアップアプローチで、仕様モデル及び検証対象プログラムの間の条件分岐経路の整合性を判定する。詳細は、後述する（図１４、図１５参照）。
【００３１】
ボトムアップ全体整合性判定部１３５（第２の整合性判定部の一例）は、カットセット表に基づき、仕様モデルの条件分岐経路と出力演算値との組み合わせの全パターンが、検証対象プログラムの条件分岐経路と出力演算値との組み合わせの全パターンと整合しているか否かを判定する。つまり、ボトムアップ全体整合性判定部１３５は、検証対象プログラム側からのボトムアップアプローチで、仕様モデル及び検証対象プログラムの間の条件分岐経路と出力演算値との組み合わせの整合性（全体整合性）を判定する。詳細は、後述する（図１６参照）。
【００３２】
検証部１３６は、各判定部１３１〜１３５の判定結果に基づき、仕様モデルと検証対象プログラムの一致性を検証する。詳細は、後述する（図３参照）。
【００３３】
［情報処理装置による処理の詳細］
次に、図３〜図１６を参照して、情報処理装置１０による検証対象プログラムの仕様モデルに対する一致性を検証する処理（以下、「一致性検証処理」）について説明する。
【００３４】
図３は、情報処理装置１０による一致性検証処理の一例を示すフロー図である。本例では、情報処理装置１０は、検証対象プログラム３１０が、ベースとなる仕様モデル３００を満足しているか否か、つまり、検証対象プログラム３１０の仕様モデル３００に対する一致性を検証する。
【００３５】
尚、図３では、参考として、一致性検証処理の前段階である仕様検討の工程や検証対象プログラムの実装設計の工程についても示される。
【００３６】
＜カットセット表の生成＞
図３に示すように、ステップＳ１０にて、カットセット表生成部１２は、仕様モデル３００及び検証対象プログラム３１０のそれぞれに対応するカットセット表３０１及びカットセット表３１１を生成する。以下、図４を参照して、カットセット表の内容について説明すると共に、図５〜図１０を参照して、カットセット表の生成方法について説明する。
【００３７】
図４は、カットセット表の一例を説明する図である。具体的には、図４（ａ）は、仕様モデル３００及び検証対象プログラム３１０の入出力の関係を示す概念図であり、図４（ｂ）は、図４（ａ）の入出力の関係に基づき規定されるカットセット表３０１，３１１の一例を示す図である。
【００３８】
図４（ａ）に示すように、仕様モデル及び検証対象プログラムの論理構造は、条件入力４０１（判定条件Ｃ１〜Ｃｎ）と、条件入力４０１に含まれるそれぞれの条件判定結果に応じて選択される条件分岐経路（演算経路）４０２と、選択された条件分岐経路４０２に応じて出力される出力結果４０３（出力演算値Ｆ１（Ｄ１）〜Ｆｎ（Ｄｎ））に分割されうる。
【００３９】
カットセット表生成部１２は、仕様モデル及び検証対象プログラムを条件入力４０１と、条件分岐経路４０２と、出力結果４０３に分割し、図４（ｂ）に示すように、論理構造を示すカットセット表を生成する。具体的には、カットセット表は、行インデックスとしての条件入力４０１（判定条件Ｃ１〜Ｃｎ）と、条件入力４０１のそれぞれの判定結果（"Ｔ"（True）或いは"Ｆ"（False））の組み合わせの全パターンが各列に記載される条件分岐経路４０２と、条件分岐経路４０２の下に記載される、条件分岐経路４０２の全パターンのそれぞれに対応する出力結果４０３（出力演算値Ｆ１（Ｄ１）〜Ｆｎ（Ｄｎ））により構成される。
【００４０】
図５は、カットセット表の生成対象の仕様モデル及び検証対象プログラムの一例を説明する図である。
【００４１】
図５に示すように、本例の仕様モデル及び検証対象プログラムでは、処理「ａ」５０１〜処理「ｎ」５１４の間の入出力の関係が規定されている。処理「ａ」５０１〜処理「ｎ」５１４では、それぞれ、例えば、少数、整数、文字列等の型のデータを用いて、任意の処理が行われ、任意の型のデータが出力される。図５中の矢印は、矢印の元の出力データが、矢印の先に入力されることを示す。例えば、処理「ｆ」５０６は、処理「ｅ」５０５及び処理「ａ」５０１の結果により出力されるデータが入力され、所定の処理を行い、処理結果のデータをスイッチ５５１及びスイッチ５５２に出力する。
【００４２】
スイッチ５５１〜５５６は、分岐を示す。スイッチ５５１〜５５６のそれぞれの左端中央部５５１ａ〜５５６ａは、分岐の条件を示し、例えば、Ｃ言語による検証対象プログラムのソースコードにおけるｉｆ文の条件に相当する。本例では、当該ｉｆ文の結果が真（true）であれば、左端上側部分５５１ｂ〜５５６ｂから入力されたデータが出力され、当該ｉｆ文の結果が偽（false）であれば、左端下側部分５５１ｃ〜５５６ｃから入力されたデータが出力される。
【００４３】
まず、カットセット表生成部１２は、図５に示すような仕様モデル及び検証対象プログラムに対して、プログラムスライシングを行う。プログラムスライシングとは、仕様モデルや検証対象プログラム内の所定の変数（処理）に影響を与える処理のみを、当該仕様モデル或いは検証対象プログラムから抽出する処理である。カットセット表生成部１２は、例えば、公知の技術を用いてプログラムスライシングを実行することができる。
【００４４】
例えば、図６は、プログラムスライシングの実行結果の一例を説明する図である。本例では、図５の仕様モデル或いは検証対象プログラムのプログラムスライシング結果において、例えば、図５の処理「ｊ」５１０が指定され、処理「ｊ」５１０に至る演算経路が抽出される。図６に示すように、本例のプログラムスライシング結果では、図５と比較して、処理「ｊ」５１０と無関係な処理「ｋ」５１１に至る演算経路が取り除かれている。
【００４５】
続いて、カットセット表生成部１２は、プログラムスライシング結果に基づき、依存グラフを生成する。依存グラフとは、例えば、所定の変数の出力に至るそれぞれの演算経路（処理経路）と、処理等との関係、及びそれぞれの演算経路における分岐の条件等を示すデータである。カットセット表生成部１２は、公知の技術を用いて、依存グラフを生成することができる。
【００４６】
例えば、図７は、依存グラフの一例を説明する図である。本例では、図６の演算経路６０１〜演算経路６１３と、図６の処理「ａ」５０１〜処理「ｊ」５１０との関係、及び演算経路６０１〜６１３のそれぞれにおける分岐の条件が示されている。
【００４７】
続いて、カットセット表生成部１２は、依存グラフを、一階述語論理式に変換する。カットセット表生成部１２は、公知の技術を用いて、依存グラフを一階述語論理式に変換することができる。
【００４８】
例えば、図８は、一階述語論理式の一例について説明する図であり、具体的には、図７の依存グラフに対する一階述語論理式が示される。図８中、"ｆ（ｘ、ｙ）"は、処理「ｆ」に処理「ｘ」及び処理「ｙ」の出力結果が入力されることを表す。また、"∧"は、ＡＮＤ条件を表し、"∨"は、ＯＲ条件を表す。また、"ｘ＝＝ｙ"は、"ｘ"と"ｙ"が一致することを表す。本例では、処理「ｊ」５１０に、処理「ｅ」５０５、処理「ｇ」５０７、或いは、処理「ｈ」５０８の出力結果が入力される場合の一階述語論理式が生成される。
【００４９】
尚、カットセット表生成部１２は、他の公知の技術を用いて、解析対象のデータ等から直接的に一階述語論理式を生成してもよい。
【００５０】
続いて、カットセット表生成部１２は、生成した一階述語論理式を、論理演算の法則に基づき、ＤＮＦ（Disjunctive normal form）の論理式に変換する。ＤＮＦとは、一つ以上のリテラルの論理積を一つ以上含む論理和の形式であり、「加法標準形」或いは「選言標準形」等とも称される。カットセット表生成部１２は、例えば、二重否定の除去、ド・モルガンの法則、分配法則等の論理的に等価な変換を行う論理演算の法則を用いて、一階述語論理式をＤＮＦの論理式に変換できる。
【００５１】
例えば、図９は、ＤＮＦの論理式の一例について説明する図であり、具体的には、図８の一階述語論理式に対するＤＮＦの論理式を示す。図９におけるそれぞれの記号の意味は、図８における対応する記号の意味と同様である。
【００５２】
尚、図９に示すＤＮＦの論理式と、図８に示す一階述語論理式とは、論理的に等価である。
【００５３】
続いて、カットセット表生成部１２は、変換結果として得られるＤＮＦの論理式を、選言（つまり、ＯＲ条件）を含まない、連言節（つまり、ＡＮＤ条件）で表される項（以下、「最小項」）ごとに分解する。
【００５４】
例えば、図１０は、分割された最小項の一例について説明する図であり、具体的には、図９に示すＤＮＦの論理式が、連言節（ＡＮＤ）で表される最小項ごとに分割され、ＩＤが付加されたリストを示す。
【００５５】
図１０に示すように、連言節で表現される最少項は、仕様モデル及び検証対象プログラムの出力結果である処理「ｊ」の出力データに至るまでの演算経路（条件分岐経路）を表す。具体的には、最少項の連言節で接続される各項のうち、出力データに対応する項（"ｊ＝＝ｅ（）"、"ｊ＝＝ｈ（）"、"ｊ＝＝ｇ（）"）を除く、連言節で接続される各項は、判定条件及び該判定条件に対する判定結果（"ｔｒｕｅ"或いは"ｆａｌｓｅ"）を示している。そして、最少項のリストは、入力から出力（処理「ｊ」の出力データ）に至る条件分岐経路の全パターンを表している。よって、カットセット表生成部１２は、仕様モデル及び検証対象モデルのそれぞれについて、分解された最小項のリストに基づき、条件入力４０１、条件入力４０１（条件判定群）の全パターンに相当する条件分岐経路４０２、及び、条件分岐経路４０２のそれぞれに対応する出力結果４０３を導出し、カットセット表を生成することができる。
【００５６】
＜入出力情報の整合性判定＞
図３に戻り、ステップＳ２０にて、入出力整合性判定部１３１は、仕様モデル及び検証対象プログラムのそれぞれの入力情報及び出力情報を比較し、仕様モデル及び検証対象プログラムの間に入出力の整合性があるか否かを判定する。入出力整合性判定部１３１は、仕様モデル及び検証プログラムの間に入出力の整合性がある場合、ステップＳ３０に進み、整合性がない場合、ステップＳ３０〜Ｓ６０の処理をスキップして、ステップＳ７０に進む。
【００５７】
尚、ステップＳ２０にて、仕様モデル及び検証プログラムの間に入出力の整合性がある場合、ステップＳ３０及びステップＳ５０に進み、ステップＳ３０，Ｓ４０の処理と、ステップＳ５０，Ｓ６０の処理とが並列して行われてもよい。
【００５８】
＜トップダウンでの条件分岐経路の整合性判定＞
ステップＳ３０にて、トップダウン経路整合性判定部１３２は、カットセット表に基づき、検証対象プログラムの条件分岐経路（全パターン）が、仕様モデルの条件分岐経路（全パターン）と整合しているか否かを判定する。トップダウン経路整合性判定部１３２は、検証対象プログラムの条件分岐経路が、仕様モデルの条件分岐経路と整合している場合、ステップＳ４０に進み、整合していない場合、ステップＳ４０〜Ｓ６０の処理をスキップし、ステップＳ７０に進む。以下、図１１、図１２を参照して、仕様モデルから見た検証対象プログラムの条件分岐経路の整合性を判定する方法について説明する。
【００５９】
図１１は、仕様モデルから見た検証対象プログラムの条件分岐経路の整合性判定処理（以下、「トップダウン経路整合性判定処理」）の一例を示すフロー図である。図１２は、検証対象プログラムの条件分岐経路の全パターンの中から仕様モデルの条件分岐経路に対応する条件分岐経路を抽出する方法の一例を説明する図である。
【００６０】
尚、図１２において、仕様モデルの変数"ｐ"及び変数"ｑ"と、検証対象プログラムの変数"ｒ"及び変数"ｓ"との間には、"ｐ＝ｒ"及び"ｑ＝ｓ"の関係があり、情報処理装置１０は、入出力整合性判定部１３１により出力される入出力対応関係データに基づき、当該対応関係を予め認識（把握）することができる。また、図１１、図１２に示す仕様モデル及び検証対象プログラムの互いのカットセット表の条件入力の順序（行方向の順序）は、入出力整合性判定部１３１により出力される入出力対応関係データに基づき、対応する判定条件同士が同じ行になるように整理されている。以下、図１４、図１５の仕様モデル及び検証対象プログラムについても同様である。
【００６１】
図１１に示すように、ステップＳ１１０１にて、トップダウン経路整合性判定部１３２は、仕様モデルのカットセット表から条件分岐経路（経路"Ａ"）を抽出する。そして、トップダウン経路整合性判定部１３２は、抽出した仕様モデルの条件分岐経路と、検証対象プログラムの特定の評価対象の条件分岐経路（本例では、４つの条件分岐経路のうちのカットセット表の左端の列の条件分岐経路）とが同等（一致する）かどうかを評価する。例えば、トップダウン経路整合性判定部１３２は、ＳＭＴ（Satisfiability Modulo Theories）ソルバ（述語論理に対するソルバ）を用いて、仕様モデルのカットセット表から抽出された条件分岐経路と、検証対象プログラムのカットセット表の特定の条件分岐経路とが同等であるかどうかを判定する。具体的には、トップダウン経路整合性判定部１３２は、仕様モデルのカットセット表から抽出された条件分岐経路に相当する一又は複数の判定結果の論理積と、検証対象プログラムのカットセット表の特定の条件分岐経路に相当する一又は複数の判定結果の論理積と、を論理積で接合した命題論理式を生成する。そして、トップダウン経路整合性判定部１３２は、当該命題論理式が充足可能な場合（構成する変数値によって成立する組み合わせが存在する場合）、これらの条件分岐経路が同等である（一致性がある）と判定し、充足不能な場合、同等でないと判定する。
【００６２】
例えば、図１２（ａ），（ｂ）に示す仕様モデル及び検証対象プログラムのカットセット表を前提とする。本例では、仕様モデルのカットセット表における左端の列の条件分岐経路は、検証対象プログラムのカットセット表における左からの二番目の列の条件分岐経路と同等である。この場合、図１２（ｃ）に示すように、仕様モデルのカットセット表における左端の列の条件分岐経路に相当する二つの判定結果の論理積と、検証対象プログラムの左から二番目の列の条件分岐経路に相当する二つの判定結果の論理積とが論理積で接合された命題論理式は、ＳＭＴソルバによって、充足可能と判定される。一方、図１２（ｄ）に示すように、仕様モデルのカットセット表における左端の列の条件分岐経路に相当する二つの判定結果の論理積と、検証対象プログラムのカットセット表における左から二番目の列以外（本例では、左端の列）の条件分岐経路に相当する二つの判定結果の論理積とが論理積で接合された命題論理式は、ＳＭＴソルバによって、充足不能と判定される。
【００６３】
図１１に示すように、ステップＳ１１０２にて、トップダウン経路整合性判定部１３２は、仕様モデルの条件分岐経路（経路"Ａ"）と、検証対象プログラムの評価対象の条件分岐経路（カットセット表の左端の列の条件分岐経路）とが同等である場合、これらの条件分岐経路に一致性があると判定する。
【００６４】
一方、ステップＳ１１０３にて、トップダウン経路整合性判定部１３２は、仕様モデルの条件分岐経路（経路"Ａ"）と、検証対象プログラムの評価対象の条件分岐経路（カットセット表の左端の列の条件分岐経路）とが同等でない場合、評価対象の条件分岐経路を変更して（本例では、カットセット表の左から二番目の条件分岐経路に変更して）、ステップＳ１１０１と同様の評価を継続する。
【００６５】
ステップＳ１１０４にて、トップダウン経路整合性判定部１３２は、仕様モデルの条件分岐経路（経路"Ａ"）と、検証対象プログラムの変更後の評価対象の条件分岐経路（カットセット表の左から二番目の列の条件分岐経路）とが同等である場合、ステップＳ１１０２と同様、これらの条件分岐経路に一致性があると判定する。
【００６６】
一方、ステップＳ１１０５にて、トップダウン経路整合性判定部１３２は、トップダウン経路整合性判定部１３２は、仕様モデルの条件分岐経路（経路"Ａ"）と、検証対象プログラムの変更後の評価対象の条件分岐経路（カットセット表の左からの二番目の列の条件分岐経路）とが同等でない場合、検証対象プログラムの条件分岐経路を更に変更して、ステップＳ１１０１と同様の評価を更に継続する。
【００６７】
このように、トップダウン経路整合性判定部１３２は、抽出した仕様モデルの条件分岐経路（経路"Ａ"）と同等の条件分岐経路が検証対象プログラムのカットセット表で見つかるか、或いは、検証対象プログラムにおける評価対象の条件分岐経路がなくなるまでステップＳ１１０１の評価を繰り返す。
【００６８】
ステップＳ１１０６にて、トップダウン経路整合性判定部１３２は、仕様モデルのカットセット表における残りの条件分岐経路（本例では、経路"Ｂ"〜"Ｄ"）についても、同等の条件分岐経路が検証対象プログラムのカットセット表で見つかるか、或いは、検証対象プログラムにおける評価対象の条件分岐経路がなくなるまでステップＳ１１０１と同様の評価を繰り返す。
【００６９】
尚、仕様モデルのカットセット表における条件分岐経路ごとの上述の処理は、並列で実行されてもよい。
【００７０】
ステップＳ１１０７にて、トップダウン経路整合性判定部１３２は、ステップＳ１１０１〜Ｓ１１０６の処理の結果、仕様モデルのカットセット表の全ての条件分岐経路について、同等の条件分岐経路が検証対象プログラムに存在する場合、検証対象プログラムの条件分岐経路が、仕様モデルの条件分岐経路に整合していると判定する。
【００７１】
一方、ステップＳ１１０８にて、トップダウン経路整合性判定部１３２は、ステップＳ１１０１〜Ｓ１１０６の処理の結果、仕様モデルのカットセット表の全ての条件分岐経路の少なくとも一つについて、同等の条件分岐経路が検証対象プログラムに存在しない場合、検証対象プログラムの条件分岐経路が、仕様モデルの条件分岐経路に整合していないと判定する。
【００７２】
尚、トップダウン経路整合性判定部１３２は、仕様モデルの何れかの条件分岐経路について、検証対象プログラムのカットセット表の中から同等の条件分岐経路を見つけられなかった時点で、検証対象プログラムの条件分岐経路が、仕様モデルの条件分岐経路に整合していないと判定してもよい。
【００７３】
＜トップダウンでの条件分岐経路と出力結果との組み合わせの整合性判定＞
図３に戻り、ステップＳ４０にて、トップダウン全体整合性判定部１３３は、カットセット表に基づき、検証対象プログラムの条件分岐経路と出力結果との組み合わせ（全パターン）が、仕様モデルの条件分岐経路と出力結果との組み合わせ（全パターン）に対して、整合しているか否かを判定する。トップダウン全体整合性判定部１３３は、検証対象プログラムの条件分岐経路と出力結果との組み合わせが、仕様モデルの条件分岐経路と出力結果との組み合わせと整合している場合、ステップＳ５０に進み、整合していない場合、ステップＳ５０，Ｓ６０の処理をスキップし、ステップＳ７０に進む。以下、図１３を参照し、仕様モデルから見た検証対象プログラムの条件分岐経路と出力結果の組み合わせの整合性を判定する方法について説明する。
【００７４】
図１３は、仕様モデルから見た検証対象プログラムの条件分岐経路と出力結果との組み合わせの整合性判定処理（以下、「トップダウン全体整合性判定処理」）の一例を示すフロー図である。
【００７５】
図１３に示すように、ステップＳ１３０１にて、トップダウン全体整合性判定部１３３は、仕様モデルのカットセット表から条件分岐経路（経路"Ａ"）を抽出し、当該条件分岐経路に対応する（当該条件分岐経路を通過する）評価パターン（テストケース）を、当該条件分岐経路を通過するデータ入力を網羅する観点（入力網羅の観点）で一又は複数生成する。いわゆるＭＣ／ＤＣ（Modified Condition/Decision Coverage）の観点は、カットセット表に全ての条件分岐経路が含まれている点で達成されおり、不十分だからである。そして、トップダウン全体整合性判定部１３３は、生成した評価パターンを仕様モデルと検証対象プログラムの双方に入力し、出力結果を比較する。
【００７６】
また、ステップＳ１３０２にて、トップダウン全体整合性判定部１３３は、仕様モデルのカットセット表の残りの条件分岐経路（経路"Ｂ"〜"Ｄ"）についても、ステップＳ１３０１と同様に、対応する評価パターンを入力網羅の観点で一又は複数生成する。そして、トップダウン全体整合性判定部１３３は、ステップＳ１３０１と同様、生成した評価パターンを仕様モデルと検証対象プログラムの双方に入力し、出力結果を比較する。
【００７７】
尚、仕様モデルのカットセット表における条件分岐経路ごとの上述の処理は、並列で実行されてもよい。
【００７８】
ステップＳ１３０３にて、トップダウン全体整合性判定部１３３は、仕様モデルのカットセット表の全ての条件分岐経路に対応する評価パターンについて、仕様モデルと検証対象プログラムとの双方の出力結果が同等である場合、検証対象プログラムの条件分岐経路と出力結果との組み合わせが、仕様モデルの条件分岐経路と出力結果との組み合わせと整合していると判定する。
【００７９】
一方、ステップＳ１３０４にて、トップダウン全体整合性判定部１３３は、仕様モデルのカットセット表の全ての条件分岐経路に対応する評価パターンの少なくとも一つについて、仕様モデルと検証対象プログラムとの双方の出力結果が同等でない場合、検証対象プログラムの条件分岐経路と出力結果との組み合わせが、仕様モデルの条件分岐経路と出力結果との組み合わせと整合していないと判定する。
【００８０】
＜ボトムアップでの条件分岐経路の整合性判定＞
図３に戻り、ステップＳ５０にて、ボトムアップ経路整合性判定部１３４は、カットセット表に基づき、仕様モデルの条件分岐経路（全パターン）が、検証対象プログラムの条件分岐経路（全パターン）と整合しているか否かを判定する。ボトムアップ経路整合性判定部１３４は、仕様モデルの条件分岐経路が、検証対象プログラムの条件分岐経路と整合している場合、ステップＳ６０に進み、整合していない場合、ステップＳ６０の処理をスキップして、ステップＳ７０に進む。以下、図１４、図１５を参照して、検証対象プログラムから見た仕様モデルの条件分岐経路の整合性を判定する方法について説明する。
【００８１】
図１４は、検証対象プログラムから見た仕様モデルの条件分岐経路の整合性判定処理（以下、「ボトムアップ経路整合性判定処理」）の一例を示すフロー図である。図１５は、仕様モデルの条件分岐経路の全パターンの中から検証対象プログラムの条件分岐経路に対応する条件分岐経路を抽出する方法の一例を説明する図である。
【００８２】
図１４に示すように、ステップＳ１４０１にて、ボトムアップ経路整合性判定部１３４は、検証対象プログラムのカットセット表から条件分岐経路（経路"ａ"）を抽出する。そして、ボトムアップ経路整合性判定部１３４は、抽出した検証対象プログラムの条件分岐経路と、仕様モデルの特定の評価対象の条件分岐経路（本例では、４つの条件分岐経路のうちのカットセット表の左端の列の条件分岐経路）とが同等（一致する）かどうかを評価する。例えば、ボトムアップ経路整合性判定部１３４は、ＳＭＴソルバを用いて、検証対象プログラムのカットセット表から抽出された条件分岐経路と、仕様モデルのカットセット表の特定の条件分岐経路とが同等であるかどうかを判定する。具体的には、ボトムアップ経路整合性判定部１３４は、検証対象プログラムのカットセット表から抽出された条件分岐経路に相当する一又は複数の判定結果の論理積と、仕様モデルのカットセット表の特定の条件分岐経路に相当する一又は複数の判定結果の論理積と、を論理積で接合した命題論理式を生成する。そして、ボトムアップ経路整合性判定部１３４は、当該命題論理式が充足可能な場合、これらの条件分岐経路が同等である（一致性がある）と判定し、充足不能な場合、同等でないと判定する。
【００８３】
例えば、図１５（ａ），（ｂ）に示す検証対象プログラム及び仕様モデルのカットセット表を前提とする。本例では、検証対象プログラムのカットセット表における左端の列の条件分岐経路は、仕様モデルのカットセット表における右端の列の条件分岐経路と同等である。この場合、図１５（ｃ）に示すように、検証対象プログラムのカットセット表における左端の列の条件分岐経路に相当する二つの判定結果の論理積と、仕様モデルの右端の列の条件分岐経路に相当する二つの判定結果の論理積とが、論理積で接合された命題論理式は、ＳＭＴソルバによって、充足可能と判定される。一方、図１５（ｄ）に示すように、検証対象プログラムのカットセット表における左端の列の条件分岐経路に相当する二つの判定結果の論理積と、仕様モデルのカットセット表における右端の列以外（本例では、左端の列）の条件分岐経路に相当する二つの判定結果の論理積とが、論理積で接合された命題論理式は、ＳＭＴソルバによって、充足不能と判定される。
【００８４】
図１４に示すように、ステップＳ１４０２にて、ボトムアップ経路整合性判定部１３４は、検証対象プログラムの条件分岐経路（経路"ａ"）と、仕様モデルの評価対象の条件分岐経路（カットセット表の左端の列の条件分岐経路）とが同等である場合、これらの条件分岐経路に一致性があると判定する。
【００８５】
一方、ステップＳ１４０３にて、ボトムアップ経路整合性判定部１３４は、検証対象プログラムの条件分岐経路（経路"ａ"）と、仕様モデルの評価対象の条件分岐経路（カットセット表の左端の列の条件分岐経路）とが同等でない場合、評価対象の条件分岐経路を変更して（本例では、カットセット表の左から二番目の条件分岐経路に変更して）、ステップＳ１４０１と同様の評価を継続する。
【００８６】
ステップＳ１４０４にて、ボトムアップ経路整合性判定部１３４は、検証対象プログラムの条件分岐経路（経路"ａ"）と、仕様モデルの変更後の評価対象の条件分岐経路（カットセット表の左から二番目の列の条件分岐経路）とが同等である場合、ステップＳ１４０２と同様、これらの条件分岐経路に一致性があると判定する。
【００８７】
一方、ステップＳ１４０５にて、ボトムアップ経路整合性判定部１３４は、ボトムアップ経路整合性判定部１３４は、検証対象プログラムの条件分岐経路（経路"ａ"）と、仕様モデルの変更後の評価対象の条件分岐経路（カットセット表の左からの二番目の列の条件分岐経路）とが同等でない場合、仕様モデルの条件分岐経路を更に変更して、ステップＳ１４０１と同様の評価を更に継続する。
【００８８】
このように、ボトムアップ経路整合性判定部１３４は、抽出した検証対象プログラムの条件分岐経路（経路"ａ"）と同等の条件分岐経路が仕様モデルのカットセット表で見つかるか、或いは、仕様モデルにおける評価対象の条件分岐経路がなくなるまでステップＳ１４０１の評価を繰り返す。
【００８９】
ステップＳ１４０６にて、ボトムアップ経路整合性判定部１３４は、検証対象プログラムのカットセット表における残りの条件分岐経路（本例では、経路"ｂ"〜"ｄ"）についても、同等の条件分岐経路が仕様モデルのカットセット表で見つかるか、或いは、仕様モデルにおける評価対象の条件分岐経路がなくなるまでステップＳ１４０１の評価を繰り返す。
【００９０】
尚、検証対象プログラムのカットセット表における条件分岐経路ごとの上述の処理は、並列で実行されてもよい。
【００９１】
ステップＳ１４０７にて、ボトムアップ経路整合性判定部１３４は、ステップＳ１４０１〜Ｓ１４０６の処理の結果、検証対象プログラムのカットセット表の全ての条件分岐経路について、同等の条件分岐経路が仕様モデルに存在する場合、仕様モデルの条件分岐経路が、検証対象プログラムの条件分岐経路に整合していると判定する。
【００９２】
一方、ステップＳ１４０８にて、ボトムアップ経路整合性判定部１３４は、ステップＳ１４０１〜Ｓ１４０６の処理の結果、検証対象プログラムのカットセット表の全ての条件分岐経路の少なくとも一つについて、同等の条件分岐経路が仕様モデルに存在しない場合、仕様モデルの条件分岐経路が、検証対象プログラムの条件分岐経路に整合していないと判定する。
【００９３】
尚、ボトムアップ経路整合性判定部１３４は、検証対象プログラムの何れかの条件分岐経路について、仕様モデルのカットセット表の中から同等の条件分岐経路を見つけられなかった時点で、仕様モデルの条件分岐経路の条件分岐経路が、検証対象のプログラムの条件分岐経路に整合していないと判定してもよい。
【００９４】
＜ボトムアップでの条件分岐経路と出力結果との組み合わせの整合性判定＞
図３に戻り、ステップＳ６０にて、ボトムアップ全体整合性判定部１３５は、カットセット表に基づき、仕様モデルの条件分岐経路と出力結果との組み合わせ（全パターン）が、検証対象プログラムの条件分岐経路と出力結果との組み合わせ（全パターン）に対して、整合しているか否かを判定する。ボトムアップ全体整合性判定部１３５は、当該判定が終了すると、ステップＳ７０に進む。以下、図１６を参照し、検証対象プログラムから見た仕様モデルの条件分岐経路と出力結果の組み合わせの整合性を判定する方法について説明する。
【００９５】
図１６は、検証対象プログラムから見た仕様モデルの条件分岐経路と出力結果との組み合わせの整合性判定処理（以下、「ボトムアップ全体整合性判定処理」）の一例を示すフロー図である。
【００９６】
図１６に示すように、ステップＳ１６０１にて、ボトムアップ全体整合性判定部１３５は、検証対象プログラムのカットセット表から条件分岐経路（経路"ａ"）を抽出し、当該条件分岐経路に対応する（当該条件分岐経路を通過する）評価パターン（テストケース）を、当該条件分岐経路を通過するデータ入力を網羅する観点（入力網羅の観点）で一又は複数生成する。上述の如く、いわゆるＭＣ／ＤＣの観点は、カットセット表に全ての条件分岐経路が含まれている点で達成されおり、不十分だからである。そして、ボトムアップ全体整合性判定部１３５は、生成した評価パターンを検証対象プログラムと仕様モデルの双方に入力し、出力結果を比較する。
【００９７】
また、ステップＳ１６０２にて、ボトムアップ全体整合性判定部１３５は、検証対象プログラムのカットセット表の残りの条件分岐経路（経路"ｂ"〜"ｄ"）についても、ステップＳ１６０１と同様に、対応する評価パターンを入力網羅の観点で一又は複数生成する。そして、ボトムアップ全体整合性判定部１３５は、ステップＳ１６０１と同様、生成した評価パターンを検証対象プログラムと仕様モデルの双方に入力し、出力結果を比較する。
【００９８】
尚、検証対象プログラムのカットセット表における条件分岐経路ごとの上述の処理は、並列で実行されてもよい。
【００９９】
ステップＳ１６０３にて、ボトムアップ全体整合性判定部１３５は、検証対象プログラムのカットセット表の全ての条件分岐経路に対応する評価パターンについて、検証対象プログラムと仕様モデルとの双方の出力結果が同等である場合、仕様モデルの条件分岐経路と出力結果との組み合わせが、検証対象プログラムの条件分岐経路と出力結果との組み合わせと整合していると判定する。
【０１００】
一方、ステップＳ１６０４にて、ボトムアップ全体整合性判定部１３５は、検証対象プログラムのカットセット表の全ての条件分岐経路に対応する評価パターンの少なくとも一つについて、検証対象プログラムと仕様モデルとの双方の出力結果が同等でない場合、仕様モデルの条件分岐経路と出力結果との組み合わせが、検証対象プログラムの条件分岐経路と出力結果との組み合わせと整合していないと判定する。
【０１０１】
＜検証対象プログラムの仕様モデルに対する一致性の検証結果＞
ステップＳ７０にて、検証部１３６は、ステップＳ２０〜Ｓ６０の判定結果に基づき、検証対象プログラムが仕様モデルを満足しているか否か、つまり、仕様モデルと検証プログラムとの間に一致性があるか否かを検証する。具体的には、検証部１３６は、ステップＳ２０〜Ｓ６０の全てにおいて、整合している（整合あり）と判定された場合、仕様モデルと検証対象プログラムとの間に一致性があると判定する。一方、ステップＳ２０〜Ｓ６０の少なくとも一つでも整合していない（不整合あり）と判定された場合、仕様モデルと検証対象プログラムとの間に一致性がないと判定する。
【０１０２】
尚、検証部１３６は、ステップＳ４０，Ｓ６０、つまり、トップダウン全体整合性判定部１３３及びボトムアップ全体整合性判定部１３５による判定結果だけで、仕様モデルと検証対象プログラムとの間の一致性を検証してもよい。上述の如く、ステップＳ４０は、ステップＳ２０，Ｓ３０にて、整合ありと判定されることが前提となる判定処理であり、ステップＳ６０は、ステップＳ２０，Ｓ５０にて、整合ありと判定されることが前提となる処理だからである。この場合、検証部１３６は、トップダウン全体整合性判定部１３３（ステップＳ４０）及びボトムアップ全体整合性判定部１３５（ステップＳ６０）の双方で、整合していると判定された場合に、仕様モデルと検証対象プログラムとの間に一致性があると判定する。一方、検証部１３６は、トップダウン全体整合性判定部１３３（ステップＳ４０）及びボトムアップ全体整合性判定部１３５（ステップＳ６０）の何れか一方で、整合していないと判定された場合に、仕様モデルと検証対象プログラムとの間に一致性がないと判定する。
【０１０３】
［本実施形態に係る情報処理装置の作用］
次に、図１７を参照して、本実施形態に係る情報処理装置１０の作用について説明する。
【０１０４】
図１７は、本実施形態に係る情報処理装置１０の作用を説明する図である。具体的には、図１７は、仕様モデルと検証対象プログラムの一致性検証の方法を説明する図である。
【０１０５】
本実施形態では、トップダウン全体整合性判定部１３３は、検証対象プログラムの入力から出力までの条件分岐経路の全パターン、及び、該条件分岐経路の全パターンのそれぞれに対応する出力演算値により構成される（例えば、表形式の）カットセットが、検証対象プログラムのベースとなる仕様モデルのカットセットと整合しているか否かを判定する。また、ボトムアップ全体整合性判定部１３５は、仕様モデルのカットセットが、検証対象プログラムのカットセットと整合しているか否かを判定する。そして、検証部１３６は、トップダウン全体整合性判定部１３３及びボトムアップ全体整合性判定部１３５の判定結果に基づき、検証対象プログラムが仕様モデルと一致しているか（満足しているか）否かを検証する。
【０１０６】
これにより、情報処理装置１０は、仕様モデル及び検証対象プログラムのそれぞれの、条件分岐経路の全パターン及び条件分岐経路の全パターンのそれぞれに対応する出力演算値（出力結果）により構成されるカットセットの間の整合性に基づき、一致性を検証する。そのため、情報処理装置１０は、仕様を実現するための具体的な構成要素の内容に依らず、検証対象プログラムの仕様に対する一致性検証を実行できる。従って、情報処理装置１０は、より効率的にプログラムの仕様に対する一致性検証を行うことができる。
【０１０７】
具体的には、図１７に示すように、本実施形態では、情報処理装置１０は、仕様モデルと検証対象プログラムとの間で、カットセット表を用いて、条件分岐経路の整合性（図３のステップＳ３０，Ｓ５０）と、出力結果（出力演算値）の整合性（図３のステップＳ２０）を判定（確認）する。そして、情報処理装置１０は、仕様モデルと検証対象プログラムとの間で、条件分岐経路及び出力結果（出力演算値）の単独での整合性があることを確認した上で、条件分岐経路と出力結果との間の組み合わせの整合性を判定（確認）する。これにより、条件分岐経路に対応する評価パターンだけが生成されるため、仕様モデルと検証対象プログラムとの間の一致性検証のために生成する評価パターン（テストケース）の数を大幅に削減することができ、効率的な検証作業を実現することができる。
【０１０８】
また、本実施形態では、情報処理装置１０は、カットセット表を用いて、仕様モデルから見た一致性検証（つまり、トップダウンアプローチの一致性検証）と、検証対象プログラムから見た一致性検証（つまり、ボトムアップアプローチの一致性検証）の両面を担保する。これにより、仕様モデル側及び検証対象モデル側の双方から見て、条件分岐経路が過不足なく存在する点等を評価することができるため、無駄の少ない一致性検証を実現することができる。
【０１０９】
以上、本発明を実施するための形態について詳述したが、本発明はかかる特定の実施形態に限定されるものではなく、特許請求の範囲に記載された本発明の要旨の範囲内において、種々の変形・改良が可能である。
【０１１０】
例えば、上述の実施形態において、情報処理装置１０の各機能部は、一以上のコンピュータにより構成されるクラウドコンピューティングにより実現されてもよい。
【符号の説明】
【０１１１】
１０  情報処理装置
１１  取得部
１２  カットセット表生成部
１３  一致性検証部
１３１  入出力整合性判定部
１３２  トップダウン経路整合性判定部
１３３  トップダウン全体整合性判定部（第１の整合性判定部）
１３４  ボトムアップ経路整合性判定部
１３５  ボトムアップ全体整合性判定部（第２の整合性判定部）
１３６  検証部
【図１】
2019197329.tif 000003
【図２】
2019197329.tif 000004
【図３】
2019197329.tif 000005
【図４】
2019197329.tif 000006
【図５】
2019197329.tif 000007
【図６】
2019197329.tif 000008
【図７】
2019197329.tif 000009
【図８】
2019197329.tif 000010
【図９】
2019197329.tif 000011
【図１０】
2019197329.tif 000012
【図１１】
2019197329.tif 000013
【図１２】
2019197329.tif 000014
【図１３】
2019197329.tif 000015
【図１４】
2019197329.tif 000016
【図１５】
2019197329.tif 000017
【図１６】
2019197329.tif 000018
【図１７】
2019197329.tif 000019