(57)【要約】【課題】形式手法によってソフトウェアの設計情報に不整合がないことを自動的に検証することを、確実に行う。【解決手段】形式検証支援装置３０は、ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、ソフトウェアが実行を開始してから終了するまでに行う代入処理の処理内容を表す仕様情報を抽出する抽出部３３と、抽出部３３によって抽出された、特定の変数へ値を代入する１以上の代入処理について、特定の変数を、代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、特定の変数に関して最後に行われる代入処理である最終代入処理の後に、最終代入処理において置き換えられた局所変数の値を特定の変数に代入する代入処理を追加する内容に、仕様情報を更新する更新部３４と、を備える。【選択図】      図１４
2017107347.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、前記ソフトウェアが実行を開始してから終了するまでに行う前記代入処理の処理内容を表す仕様情報を抽出する抽出手段と、
前記抽出手段によって抽出された、特定の前記変数へ値を代入する１以上の前記代入処理について、前記特定の変数を、前記代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、前記特定の変数に関して最後に行われる前記代入処理である最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する更新手段と、
を備える形式検証支援装置。
【請求項２】
前記抽出手段は、条件分岐を含む処理を実行する前記ソフトウェアが実行を開始してから終了するまでに行う複数の情報処理パスに関する情報を含む前記設計情報から、前記複数の情報処理パスに関する前記仕様情報を抽出し、
前記更新手段は、前記情報処理パスごとに、前記特定の変数を前記代入処理ごとに異なる前記局所変数に置き換えるとともに、前記最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する、
請求項１に記載の形式検証支援装置。
【請求項３】
前記抽出手段は、前記特定の変数の値を参照する参照処理に関する情報を含む前記設計情報から、前記参照処理ごとの前記仕様情報を抽出し、
前記更新手段は、前記特定の変数を、前記代入処理ごとに異なる前記局所変数に置き換えることに応じて、前記参照処理に含まれる前記特定の変数を前記局所変数に置き換える内容に、前記仕様情報を更新する、
請求項１または２に記載の形式検証支援装置。
【請求項４】
前記ソフトウェアにおける前記参照処理の内容に応じて前記条件分岐あるいは合流を行うパス制御処理、及び、前記代入処理を含む前記設計情報から、前記パス制御処理及び前記代入処理をノードとして抽出することによってノード情報を生成し、前記ソフトウェアが前記ノードが示す処理を行う順序関係を表す、前記ノード間の接続をフローとして抽出することによってフロー情報を生成する設計情報処理手段
をさらに備える、請求項３に記載の形式検証支援装置。
【請求項５】
前記設計情報処理手段は、前記フローを識別可能なフロー識別子と、前記フローの始点となる前記ノードを識別可能な入力ノード識別子と、前記フローの終点となる前記ノードを識別可能な出力ノード識別子と、を関連付けた前記フロー情報を生成し、
前記抽出手段は、前記フロー情報において、第一の前記フローに関する前記出力ノード識別子を前記入力ノード識別子とする第二の前記フローを探索することを繰り返し行うことによって、前記情報処理パスを表すパス情報を生成する、
請求項４に記載の形式検証支援装置。
【請求項６】
前記抽出手段は、前記ノード情報と、前記フロー情報と、前記パス情報とに基づいて、前記情報処理パスごとに、前記代入処理あるいは前記参照処理を表す数式と、前記代入処理と前記参照処理とを区分する式区分情報と、を関連付けた前記仕様情報を生成し、
前記更新手段は、前記数式に含まれる前記特定の変数を前記局所変数に置き換え、前記最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を表す前記数式を追加し、前記式区分情報に前記局所変数であることを設定した前記局所変数を表す情報を追加することによって、前記仕様情報を更新する、
請求項５に記載の形式検証支援装置。
【請求項７】
前記更新手段は、前記特定の変数に関する前記代入処理が行われる度に１加算する代入回数情報を記憶し、前記特定の変数を、前記特定の変数の名称に前記代入回数情報が示す値を付加した名称を有する前記局所変数に置き換える、
請求項１乃至６のいずれか一項に記載の形式検証支援装置。
【請求項８】
前記更新手段によって更新された前記仕様情報を、構文規則情報に基づいて、形式検証を実行可能な形式仕様情報に変換する変換手段
をさらに備える、請求項１乃至７のいずれか一項に記載の形式検証支援装置。
【請求項９】
情報処理装置によって、
ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、前記ソフトウェアが実行を開始してから終了するまでに行う前記代入処理の処理内容を表す仕様情報を抽出し、
抽出された、特定の前記変数へ値を代入する１以上の前記代入処理について、前記特定の変数を、前記代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、前記特定の変数に関して最後に行われる前記代入処理である最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する、
形式検証支援方法。
【請求項１０】
ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、前記ソフトウェアが実行を開始してから終了するまでに行う前記代入処理の処理内容を表す仕様情報を抽出する抽出処理と、
前記抽出処理によって抽出された、特定の前記変数へ値を代入する１以上の前記代入処理について、前記特定の変数を、前記代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、前記特定の変数に関して最後に行われる前記代入処理である最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する更新処理と
をコンピュータに実行させるための形式検証支援プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本願発明は、ソフトウェアの設計情報に対する形式検証を支援する技術に関する。
【背景技術】
【０００２】
ソフトウェアの開発では、ソフトウェアの品質を確保するために、その設計内容が正しいことを検証する必要がある。そのため、ソフトウェアの開発において、その設計情報をＵＭＬ（Unified Modeling Language）により記述したり、あるいは、形式手法により検証したりすることが行われている。ＵＭＬは、ソフトウェアが行う処理の流れを、例えばアクティビティ図を用いて図式的に表す記法である。形式手法は、集合や論理といった数学的な概念に基づいて、対象システムを正確かつ曖昧さのない記法により表現し、設計情報に不整合がないことを検証する手法である。
【０００３】
逐次処理を行うソフトウェアの設計では、当該ソフトウェアが行う処理の流れを、フローチャートあるいはＵＭＬによるアクティビティ図等により表現する。逐次処理を表すアクティビティ図は、処理の各ステップをノードとして表現する。このノードには、処理全体の開始を表す開始ノード、処理全体の終了を表す終了ノード、処理ステップとして処理の流れの分岐を表すディシジョンノード、処理ステップとして処理の流れの合流を表すマージノード、及び、処理ステップとしてデータの変更すなわち変数への値の代入を表すアクションノード等がある。
【０００４】
このような図により表現された設計内容が正しいかどうかは、通常、人手作業により検証されている。したがって、検証を行う人の技術的なスキルが低ければ、欠陥の多くを見逃す可能性がある。このような問題に対して、例えば、形式手法の１つであるEvent-Bでは、ソフトウェアの設計内容を、集合や一階述語論理（数理論理学における論理の数学的モデルの一つであり）の式により記述し、複数の式の間において整合がとれていることをツールの支援を受けながら数学的に証明することにより、Event-Bの記述に欠陥がないことを保証する。
【０００５】
Event-Bでは、データを定数や変数として、データに関する制約を不変条件として、データを操作する処理をイベント（以降、「Event-Bイベント」と称す）として表す。Event-Bイベントは、ガード節とアクション節とから構成される。ガードとは、ソフトウェアが行う処理の流れである制御フローにおいて、後続のノードを実行できるかを確認する条件のことである。そして、ガード節に記述された全ての論理式（以降、「Event-Bガード」と称す）が真となる場合のみ、アクション節に記述された全ての代入式（以降、「Event-Bアクション」と称す）が実行される。整合性を示す重要な条件の１つとして不変条件保存則がある。この不変条件保存則は、Event-Bイベント及び不変条件の組ごとに、当該不変条件が成り立っている任意の状態から、当該Event-Bイベントを実行した後の状態において、再び当該不変条件が成り立つことである（非特許文献１参照）。
【０００６】
このような形式手法に関する技術の一例として、特許文献１には、アクティビティ図により表された逐次処理とクラス図により表されたデータとの間に不整合がないことをEvent-Bを用いて検証する装置が開示されている。この装置は、アクティビティ図におけるノードをEvent-Bイベントと関連付け、ノードが行う処理の結果を「局所事後条件」と称する論理式（状態が真あるいは偽であることを示す式）により表現することにより、Event-Bによる記述に変換する。
【０００７】
また、特許文献２には、ＵＭＬクラス図とアクティビティ図により記述した設計モデルを読み込み、その設計モデルからアクティビティ図をテスト対象として抽出し、テスト対象から実行経路を抽出するテストデータ生成装置が開示されている。この装置は、抽出された各実行経路の制約条件に基づいて、テストデータ仕様を更新する。この装置は、テストデータ仕様を読み込み、因子毎に「水準」を生成し、因子と水準の組み合わせである「入力」に対する実行経路を取得する。この装置は、「入力」が正常入力（実行経路にとって許容する入力）または異常入力（当該実行経路にとって許容しない入力）であるか、及び、実行経路中に事後条件が含まれるか否かによって期待値を求め、「入力」に当該期待値を付与したテストデータを生成する。
【０００８】
また、特許文献３には、ソフトウェアの仕様が、意味規則及び構文規則によって定義された形式言語で記述された形式仕様であって、その形式仕様が要求された検証項目を満たすか否かを、意味規則に基づいた所定の検証方法によって検証する設計支援方法が開示されている。この方法は、形式仕様が検証項目を満たさない場合は、形式仕様に含まれる誤り箇所を特定し、形式仕様の記述、及び、所定の検証方法によって形式仕様が検証された履歴の少なくとも一方に基づいて、特定された誤りを修正するための修正候補を抽出し、抽出された修正候補を出力する。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開2014-241051号公報
【特許文献２】特開2010-267023号公報
【特許文献３】特開2009-116648号公報
【非特許文献】
【００１０】
【非特許文献１】C. Metayer, J.-R. Abrial, L. Voisin, "RODIN Deliverable 3.2 Event-B Language," RODIN (Rigorous Open Development Environment for Complex Systems), Project IST-511599, 31st May 2005
【発明の概要】
【発明が解決しようとする課題】
【００１１】
特許文献１が示す技術では、処理ステップの結果を表す局所事後条件を導入することにより、証明への入力となる論理式が増加する。この場合、論理式の間における不整合を自動的に検証することが困難になる。すなわち、例えば、開始ノードからｍ（ｍは任意の自然数）ステップ目のノードにおいて変数ｘに１を設定し、後続のｎ（ｎは任意の自然数）ステップ目のノードでｘに別の値を設定するのであれば、ｍステップ目のノードに関する局所事後条件は「ｘ＝１」である。この局所事後条件は、ｎステップ目のノードが実行される直前まで成立しなければならない。この局所事後条件を、例えば特許文献１が示す装置は、ステップがｍ以上かつｎ未満であればｘは１であることを示す「（ｍ≦ステップ ∧ ステップ＜ｎ）⇒（ｘ＝１）」というEvent-Bの不変条件として生成する。すなわち、この技術では、代入式の個数分だけ局所事後条件が生成される。設計情報における整合性を証明する定理証明器は、与えられた不変条件が、元々の設計情報の整合を確認するための条件であるか、あるいは、局所事後条件であるかを判別できない。したがって、ある不変条件がEvent-Bイベントの実行前後で成立することを証明しようとする際に、証明に無関係な多くの局所事後条件の存在が、必要な不変条件を抽出するときに障害となるという問題がある。必要な不変条件を確実に抽出できなければ、設計情報における整合性を確実に証明することはできない。特許文献１乃至３及び非特許文献は１、この問題を解決可能な技術を開示していない。本願発明の主たる目的は、この問題を解決した形式検証支援装置を提供することである。
【課題を解決するための手段】
【００１２】
本願発明の一態様に係る形式検証支援装置は、ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、前記ソフトウェアが実行を開始してから終了するまでに行う前記代入処理の処理内容を表す仕様情報を抽出する抽出手段と、前記抽出手段によって抽出された、特定の前記変数へ値を代入する１以上の前記代入処理について、前記特定の変数を、前記代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、前記特定の変数に関して最後に行われる前記代入処理である最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する更新手段と、を備える。
【００１３】
上記目的を達成する他の見地において、本願発明の一態様に係る形式検証支援方法は、情報処理装置によって、ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、前記ソフトウェアが実行を開始してから終了するまでに行う前記代入処理の処理内容を表す仕様情報を抽出し、抽出された、特定の前記変数へ値を代入する１以上の前記代入処理について、前記特定の変数を、前記代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、前記特定の変数に関して最後に行われる前記代入処理である最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する。
【００１４】
また、上記目的を達成する更なる見地において、本願発明の一態様に係る形式検証支援プログラムは、ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、前記ソフトウェアが実行を開始してから終了するまでに行う前記代入処理の処理内容を表す仕様情報を抽出する抽出処理と、前記抽出処理によって抽出された、特定の前記変数へ値を代入する１以上の前記代入処理について、前記特定の変数を、前記代入処理同士で互いに異なる新たな変数である局所変数に置き換えるとともに、前記特定の変数に関して最後に行われる前記代入処理である最終代入処理の後に、前記最終代入処理において置き換えられた前記局所変数の値を前記特定の変数に代入する前記代入処理を追加する内容に、前記仕様情報を更新する更新処理と、をコンピュータに実行させるためのプログラムである。
【００１５】
更に、本願発明は、係る形式検証支援プログラム（コンピュータプログラム）が格納された、コンピュータ読み取り可能な、不揮発性の記録媒体によっても実現可能である。
【発明の効果】
【００１６】
本願発明は、形式手法によってソフトウェアの設計情報に不整合がないことを自動的に検証することを、確実に行うことを可能とする。
【図面の簡単な説明】
【００１７】
【図１】本願発明の第１の実施形態に係る形式検証支援装置１０の構成を示すブロック図である。
【図２】本願発明の第１の実施形態に係る設計情報２００の構成を例示する図である。
【図３】本願発明の第１の実施形態に係るノード情報２１０の構成を例示する図である。
【図４】本願発明の第１の実施形態に係るフロー情報２２０の構成を例示する図である。
【図５】本願発明の第１の実施形態に係るパス情報２３０の構成を例示する図である。
【図６】本願発明の第１の実施形態に係る更新前仕様情報２４０の構成を例示する図である。
【図７】本願発明の第１の実施形態に係る更新前仕様情報２５０の構成を例示する図である。
【図８】本願発明の第１の実施形態に係る形式仕様情報２６０の構成を例示する図である。
【図９】本願発明の第１の実施形態に係る形式検証支援装置１０の動作全体を示すフローチャートである。
【図１０】本願発明の第１の実施形態に係る形式検証支援装置１０がパス情報２３０を生成する動作の詳細を示すフローチャートである。
【図１１】本願発明の第１の実施形態に係る形式検証支援装置１０がパス情報２３０を生成する際に、パスの探索を行う動作の詳細を示すフローチャートである。
【図１２】本願発明の第１の実施形態に係る形式検証支援装置１０が更新前仕様情報２４０を生成する動作の詳細を示すフローチャートである。
【図１３Ａ】本願発明の第１の実施形態に係る形式検証支援装置１０が更新前仕様情報２４０を更新後仕様情報２５０に更新する動作の詳細を示すフローチャート（１／２）である。
【図１３Ｂ】本願発明の第１の実施形態に係る形式検証支援装置１０が更新前仕様情報２４０を更新後仕様情報２５０に更新する動作の詳細を示すフローチャート（２／２）である。
【図１４】本願発明の第２の実施形態に係る形式検証支援装置３０の構成を示すブロック図である。
【図１５】本願発明の各実施形態に係る形式検証支援装置を実行可能な情報処理装置の構成を示すブロック図
【発明を実施するための形態】
【００１８】
以下、本願発明の実施の形態について図面を参照して詳細に説明する。
【００１９】
＜第１の実施形態＞
図１は、本願発明の第１の実施の形態に係る形式検証支援装置１０を概念的に示すブロック図である。形式検証支援装置１０は、記憶装置２０に格納されたソフトウェアの設計情報２００から、設計情報２００に不整合がないことを形式手法によって確実に自動検証することができる形式仕様情報２６０を生成する装置である。
【００２０】
図１に示す記憶装置２０は、磁気ディスクあるいは電子メモリ等の記憶デバイスを備えた装置であり、以下の情報を格納している。
・設計情報２００、
・ノード情報２１０、
・フロー情報２２０、
・パス情報２３０、
・更新前仕様情報２４０、
・更新後仕様情報２５０、
・形式仕様情報２６０。
これらの情報の詳細については後述する。記憶装置２０は、形式検証支援装置１０に内蔵される場合もある。
【００２１】
本実施形態に係る形式検証支援装置１０は、以下の構成を備えている。
・設計情報処理部１１、
・パス情報抽出部１２、
・仕様情報抽出部１３、
・更新部１４、
・変換部１５。
【００２２】
設計情報処理部１１、パス情報抽出部１２、仕様情報抽出部１３、更新部１４、及び、変換部１５は、電子回路の場合もあれば、コンピュータプログラムとそのコンピュータプログラムに従って動作するプロセッサによって実現される場合もある。
【００２３】
設計情報処理部１１は、記憶装置２０から設計情報２００を読み込む。図２は、設計情報２００の構成を例示する図である。図２に例示する通り、設計情報２００は、アクティビティ情報２０１、変数定義情報２０２、及び、不変条件情報２０３を含んでいる。
【００２４】
図２に例示するアクティビティ情報２０１は、その内容をアクティビティ図として図式的に表現したものである。アクティビティ図は、ソフトウェアが行う処理の各ステップを表すノードと、係る処理において先行するノードと後続のノードとを接続する有効線分により表される制御フロー（以降、「フロー」と称する）とを含んでいる。すなわち、アクティビティ図は、ノード及びフローによって、複数の処理ステップが連続して行われることを表現する。
【００２５】
アクティビティ情報２０１における開始ノード２０１０及び終了ノード２０１６は、順に、ソフトウェアの処理の開始及び終了を表すノードである。ディシジョンノード２０１１は、条件分岐を表すノードであり、開始ノード２０１０に後続するノードである。ディシジョンノード２０１１における分岐条件を示すガードは、ディシジョンノード２０１１と、その後続ノードであるアクションノード２０１２及び２０１３とを接続するフローを示す有効線分の近傍に、”[論理式]”の形式により記述されている。図２に示す例では、ソフトウェアの処理は、[ｘ＝０]が成立する場合はアクションノード２０１２へ分岐し、[ｘ≠０]が成立する場合は、アクションノード２０１３へ分岐する。
【００２６】
アクションノード２０１２及び２０１３は、変数に値を代入するアクションを表すノードであり、アクションノード２０１２及び２０１３を示すシンボル内に、そのアクションを、”{代入式の並び}”の形式により記述されている。図２に示す例では、アクションノード２０１２は、アクションの名称が「Ａ」であり、アクションの内容を表す代入式「ｙ：＝０」（「：＝」は代入を表す演算符号）に従って、変数ｙに値「０」を設定する。同様に、アクションノード２０１３は、アクションの名称が「Ｂ」であり、アクションの内容を表す代入式「ｙ：＝ｘ」に従って、変数ｙに変数ｘの値を設定する。
【００２７】
マージノード２０１４は、合流を表すノードであり、アクションノード２０１２及び２０１３に後続するノードである。すなわち、アクティビティ情報２０１が示す処理では、ディシジョンノード２０１１において分岐した処理が、マージノード２０１４において合流する。マージノード２０１４に後続するアクションノード２０１５は、アクションの名称が「Ｃ」であり、アクションの内容を表す代入式「ｙ：＝ｙ＋１」に従って、変数ｙに１を加算する。終了ノード２０１６は、アクションノード２０１５に後続し、ここでソフトウェアの処理は終了する。
【００２８】
図２に例示する変数定義情報２０２は、アクティビティ情報２０１において使用される変数について、その型及び初期値を定義する情報である。図２に例示する変数定義情報２０２は、「変数名：型＝初期値」という表記形式を使用している。すなわち、変数定義情報２０２における「ｘ：ｉｎｔ＝０」は、変数ｘの型が「ｉｎｔ（整数）」でありその初期値が「０」であることを示している。同様に、変数定義情報２０２における「ｙ：ｉｎｔ＝１」は、変数ｙの型が「ｉｎｔ」でありその初期値が「１」であることを示している。
【００２９】
図２に例示する不変条件情報２０３は、ソフトウェアがアクティビティ情報２０１に示す処理を実行する前後において、成立すべき条件を論理式によって定義する情報である。すなわち、不変条件情報２０３における「ｘ＜ｙ」は、ソフトウェアがアクティビティ情報２０１に示す処理を実行する前後において、変数ｘの値が変数ｙの値未満であることが成立しなければいけないことを示している。ソフトウェアがアクティビティ情報２０１に示す処理を実行する前後において、不変条件情報２０３が示す条件が成立しない場合は、設計情報２００に不整合が存在する。
【００３０】
設計情報処理部１１は、読み込んだ設計情報２００に基づいて、ノード情報２１０及びフロー情報２２０を生成したのち、生成したノード情報２１０及びフロー情報２２０を、記憶装置２０へ格納する。ノード情報２１０及びフロー情報２２０は、順に、アクティビティ情報２０１に含まれるノード及びフローに関する仕様を表す情報（仕様情報）である。
【００３１】
図３は、ノード情報２１０の構成例を示す。図３に示す通り、ノード情報２１０は、ノード識別子と、ノード種別と、アクション内容とをノードごとに関連付けた情報である。ノード情報２１０におけるノード識別子は、アクティビティ情報２０１に含まれる個々のノードを識別可能な識別子であり、設計情報処理部１１によって付与される。図３に示す例の場合、アクティビティ情報２０１に含まれる７個のノードに対して、「ｎ０」乃至「ｎ６」という識別子が付与されている。ノード情報２１０におけるノード種別は、アクティビティ情報２０１に含まれる各ノードが、開始ノード、終了ノード、ディシジョンノード、マージノード、及び、アクションノードのうちの何れかであるのかを示す情報である。ノード情報２１０におけるアクション内容は、アクティビティ情報２０１に含まれるアクションノードについて、アクションの内容（代入式）を示す情報である。図３に示す例の場合、アクションノード２０１２（ノード識別子：ｎ２）、アクションノード２０１３（ノード識別子：ｎ３）、及び、アクションノード２０１５（ノード識別子：ｎ５）について、そのアクション内容が格納されている。
【００３２】
図４は、フロー情報２２０の構成例を示す。図４に示す通り、フロー情報２２０は、フロー識別子と、入力ノード識別子と、出力ノード識別子と、ガード内容とをフローごとに関連付けた情報である。フロー情報２２０におけるフロー識別子は、アクティビティ情報２０１に含まれる個々のフローを識別可能な識別子であり、設計情報処理部１１によって付与される。図４に示す例の場合、アクティビティ情報２０１に含まれる７個のフローに対して、「ｆ１」乃至「ｆ７」という識別子が付与されている。フロー情報２２０における入力ノード識別子及び出力ノード識別子は、順に、フローの始点及び終点となるノードの識別子を示す情報である。フロー情報２２０におけるガード内容は、ガードが設定されているフローについて、そのガードの内容（論理式）を示す情報である。図４に示す例の場合、フローｆ２及びｆ３について、そのガード内容が格納されている。
【００３３】
図１に示すパス情報抽出部１２は、記憶装置２０からフロー情報２２０を読み込み、読み込んだフロー情報２２０に基づいてパス情報２３０を生成したのち、生成したパス情報２３０を、記憶装置２０へ格納する。パス情報２３０は、アクティビティ情報２０１が示す処理が条件分岐を含むことによって、当該処理が開始から終了に至るまでに複数のパス（情報処理パス）が存在する場合に、それらのパスの内容を示す情報である。
【００３４】
図５は、パス情報２３０の構成例を示す。図５に示す通り、パス情報２３０は、パス識別子と、フロー識別子とを関連付けた情報である。パス情報２３０におけるパス識別子は、アクティビティ情報２０１に含まれる個々のパスを識別可能な識別子であり、パス情報抽出部１１によって付与される。パス情報２３０におけるフロー識別子は、パスを構成するフローをフロー識別子により示す情報である。図２に示すアクティビティ情報２０１は、ディシジョンノード２０１１により２つのパスに分岐し、分岐したそれら２つのパスは、マージノード２０１４により合流する処理を示している。すなわち、この場合、図５のパス情報２３０が示す通り、アクティビティ情報２０１には、２つのパスが存在する。
【００３５】
パス情報抽出部１２が図４に示すフロー情報２２０に基づいて、図５に示すパス情報２３０を生成する手順について説明する。パス情報抽出部１２は、アクティビティ情報２０１が示す処理において起点となる起点ノードを探索する。この起点ノードは、フロー情報２２０において、出力ノードとして登録されていないノードとなる。パス情報抽出部１２は、この探索の結果、起点ノードの集合｛ｎ０｝を得る。
【００３６】
パス情報抽出部１２は、空の一時パスｐを生成する。パス情報抽出部１２は、フロー情報２２０において、起点ノードｎ０を入力ノードとするフローを探索し、その結果として、フローの集合｛ｆ１｝を得る。パス情報抽出部１２は、未処理のフローとしてフローｆ１を選択し、フローｆ１を一時パスに登録する。この結果として、一時パスｐはフローの列｛ｆ１｝となる。
【００３７】
パス情報抽出部１２は、一時パスｐがパス生成条件を満たすか否かを確認する。パス生成条件は、例えば記憶装置２０に格納されている（不図示）。パス生成条件は、例えば、「パスに登録されたフローの個数が上限以内である」、あるいは、「パスに登録された特定のフローの出現回数が上限以内である」、あるいは、「パスに登録されたフローについてフロー情報２２０に入力ノード登録されているノードの出現回数が上限以内である」、等の条件である。パス生成条件は、複数の条件について、論理和あるいは論理積を求めた値であってもよい。ここでは、パス生成条件は、特定のフローの出現回数が１以下であることとする。したがって、一時パスｐ｛ｆ１｝は、パス生成条件を満たす。
【００３８】
パス情報抽出部１２は、フロー情報２２０において、フローｆ１の出力ノードｎ１を入力ノードとするフローを探索し、その結果として、フローの集合｛ｆ２、ｆ３｝を得る。パス情報抽出部１２は、未処理のフローとしてフローｆ２を選択し、フローｆ２を一時パスｐに登録する。この結果として、一時パスｐは｛ｆ１、ｆ２｝となる。
【００３９】
パス情報抽出部１２は、一時パスｐがパス生成条件を満たすか否かを確認する。一時パスｐにおいて、フローｆ１及びｆ２の出現回数は１であるので、一時パスｐはパス成立条件を満たす。
【００４０】
パス情報抽出部１２は、フロー情報２２０において、フローｆ２の出力ノードｎ２を入力ノードとするフローを探索し、その結果として、フローの集合｛ｆ４｝を得る。パス情報抽出部１２は、未処理のフローとしてフローｆ４を選択し、フローｆ１を一時パスｐに登録する。この結果として、一時パスｐは｛ｆ１、ｆ２、ｆ４｝となる。
【００４１】
パス情報抽出部１２が上述した処理を再帰的に行うことにより、一時パスｐは、｛ｆ１、ｆ２、ｆ４、ｆ６、ｆ７｝となる。この時点で、パス情報抽出部１２は、フロー情報２２０において、フローｆ７の出力ノードｎ６を入力ノードとするフローを探索し、その結果として、そのようなフローが存在しないことを確認する。パス情報抽出部１２は、一時パスｐ｛ｆ１、ｆ２、ｆ４、ｆ６、ｆ７｝をパスｐ１として、パス情報２３０に登録する。
【００４２】
パス情報抽出部１２は、この後、一時パスｐから、最後尾に位置するフローｆ７を削除する。この時点で、一時パスｐは、｛ｆ１、ｆ２、ｆ４、ｆ６｝となる。パス情報抽出部１２は、フローｆ６に後続するフローの集合が｛ｆ７｝であり、フローｆ６に後続する未処理のフローが存在しないことを確認し、一時パスｐから、最後尾に位置するフローｆ６を削除する。
【００４３】
パス情報抽出部１２は、このように、一時パスｐにおいて最後尾に位置するフローに後続する未処理のフローが存在するか否かを確認し、未処理のフローが存在しない場合は、最後尾に位置するフローを一時パスｐから削除する処理を繰り返し行う。パス情報抽出部１２がこのような処理を行った結果、一時パスｐは、｛ｆ１｝となる。パス情報抽出部１２は、フロー情報２２０において、上述した処理において、フローｆ１に後続するフロー（すなわち、フローｆ１の出力ノードｎ１を入力ノードとするフロー）を探索した結果であるフローの集合｛ｆ２、ｆ３｝から、未処理のフローとしてフローｆ３を選択し、フローｆ３を一時パスｐに登録する。この結果として、一時パスｐは｛ｆ１、ｆ３｝となる。
【００４４】
パス情報抽出部１２は、一時パスｐ｛ｆ１、ｆ３｝に対して、上述と同様な処理を行うことによって、一時パスｐ｛ｆ１、ｆ３、ｆ５、ｆ６、ｆ７｝を得る。パス情報抽出部１２は、一時パスｐ｛ｆ１、ｆ３、ｆ５、ｆ６、ｆ７｝をパスｐ２として、パス情報２３０に登録することにより、図５に例示するパス情報２３０を生成し、生成したパス情報２３０を記憶装置２０へ格納する。
【００４５】
仕様情報抽出部１３は、記憶装置２０から読み出した、ノード情報２１０、フロー情報２２０、及び、パス情報２３０に基づいて、更新前仕様情報２４０を生成する。更新前仕様情報２４０は、ソフトウェアがアクティビティ情報２０１に示す処理を開始してから終了するまでに、使用する変数に対して値を代入する代入処理（すなわちアクション）及び変数の値を参照する処理（すなわちガード）の処理内容（仕様）を示す情報である。
【００４６】
図６は、図３に示すノード情報２１０、図４に示すフロー情報２２０、及び、図５に示すパス情報２３０に基づいて、仕様情報抽出部１３が生成した更新前仕様情報２４０の構成例を示す。図６に示す通り、更新前仕様情報２４０は、パス識別子と、数式識別子と、数式区分と、数式の内容と、を関連付けた情報である。
【００４７】
仕様情報抽出部１３は、図５に示すパス情報２３０に基づいて、まず、パスｐ１に存在するアクション及びガードを探索する。パスｐ１は、フローｆ１、ｆ２、ｆ４、ｆ６、ｆ７から構成されているので、仕様情報抽出部１３は、図４に示すフロー情報２２０から、これらのフローに関連付けされているガード内容を抽出する。この場合、仕様情報抽出部１３は、フローｆ２に関連付けされたガード内容「ｘ＝０」を抽出する。仕様情報抽出部１３は、フローｆ１、ｆ２、ｆ４、ｆ６、ｆ７に関する入力ノード及び出力ノードに関連付けされているアクション内容を、ノード情報２１０から抽出する。この場合、仕様情報抽出部１３は、パスｐ１に存在するノードｎ２に関連付けされたアクション内容「ｙ：＝０」と、パスｐ１に存在するノードｎ５に関連付けされたアクション内容「ｙ：＝ｙ＋１」と、を抽出する。
【００４８】
仕様情報抽出部１３は、図５に示すパス情報２３０に基づいて、同様に、パスｐ２に存在するアクション及びガードを探索する。仕様情報抽出部１３は、この場合、フローｆ３に関連付けされたガード内容「ｘ≠０」と、ノードｎ３に関連付けされたアクション内容「ｙ：＝ｘ」と、ノードｎ５に関連付けされたアクション内容「ｙ：＝ｙ＋１」と、を抽出する。
【００４９】
仕様情報抽出部１３は、抽出したガード内容及びアクション内容を、数式の内容として更新前仕様情報２４０に登録する。仕様情報抽出部１３は、この際、数式ごとに数式識別子を付与するとともに、パス識別子と、数式区分（ガードあるいはアクション）と、を関連付けて、図６に例示する通り、更新前仕様情報２４０を生成し、生成した更新前仕様情報２４０を記憶装置２０へ格納する。
【００５０】
更新部１４は、記憶装置２０から読み出した更新前仕様情報２４０を、更新後仕様情報２５０に更新する。図７は、図６に例示する更新前仕様情報２４０が、更新部１４によって更新された更新後仕様情報２５０の構成を例示する。
【００５１】
更新部１４は、図１に示す通り、代入回数情報１４０を、例えば形式検証支援装置１０が備える内部メモリに記憶している。代入回数情報１４０は、開始ノード２０１０から終了ノード２０１６に至るソフトウェアによる処理において、特定の変数に対して値を代入するアクションノードが出現した際に、当該アクションノードが、当該特定の変数について、何回目の代入処理であるのかを示す情報である。
【００５２】
更新部１４は、図６に示す更新前仕様情報２４０において、パスｐ１において最初に出現する数式ｅ１１から処理を開始する。数式ｅ１１の数式区分はガードである。そして、この時点では、アクションノードはまだ出現していないので、代入回数情報１４０は空の状態である。この場合、更新部１４は、数式ｅ１１に関しては、更新前仕様情報２４０を更新しない。
【００５３】
更新部１４は、次に、図６に示す更新前仕様情報２４０において、パスｐ１において２番目に出現する数式ｅ１２について処理を行う。数式ｅ１２の数式区分はアクションである。そして、代入回数情報１４０は空の状態である。この場合、更新部１４は、数式ｅ１２において値が代入される変数ｙについて、代入回数情報１４０を１加算して「１」に設定し、変数ｙを新たな変数である局所変数に置き換える。更新部１４は、当該局所変数の名称として、アンダースコア「＿」を挟んで、変数ｙに代入回数情報１４０が示す値を付加した名称を付与する。更新部１４は、また、数式ｅ１２における代入記号「：＝」を等号「＝」に更新するとともに、数式区分をアクションからカードに更新する。更新部１４は、上述した処理によって、図７に示す通り、数式ｅ１２の内容を「ｙ：＝０」から、「ｙ＿１＝０」に更新する。更新部１４は、さらに、新たに設定した局所変数ｙ＿１を定義するレコードとして、数式ａ１１を追加する。
【００５４】
更新部１４は、次に、図６に示す更新前仕様情報２４０において、パスｐ１において３番目に出現する数式ｅ１３について処理を行う。数式ｅ１３の数式区分はアクションである。そして、代入回数情報１４０は、変数ｙについて「１」が設定された状態である。この場合、更新部１４は、数式ｅ１３における右辺において、変数ｙを、代入回数情報１４０が示す値に従い、局所変数ｙ＿１に置き換える。更新部１４は、数式ｅ１３における左辺において、値が代入される変数ｙについて、代入回数情報１４０を１加算して「２」に設定し、変数ｙを新たな変数である局所変数に置き換える。更新部１４は、数式ｅ１２と同様の処理によって、図７に示す通り、数式ｅ１３の内容を「ｙ：＝ｙ＋１」から、「ｙ＿２＝ｙ＿１＋１」に更新する。更新部１４は、さらに、新たに設定した局所変数ｙ＿２を定義するレコードとして、数式ａ１２を追加する。
【００５５】
更新部１４は、パスｐ１について、更新前仕様情報２４０に登録されている全ての数式について処理を完了したのち、更新前仕様情報２４０における、変数ｙに値を代入する最後のアクションである数式ｅ１３において、変数ｙを置き換えた局所変数ｙ＿２の値を変数ｙに代入するアクションを示す数式ｅ１４を追加する。
【００５６】
更新部１４は、パスｐ２についても、パスｐ１と同様に、含まれる数式について順番に処理する。更新部は、以上の処理を行うことによって、図６に示す更新前仕様情報２４０を、図７に示す更新後仕様情報２５０に更新し、更新後仕様情報２５０を記憶装置２０へ格納する。
【００５７】
図１に示す変換部１５は、更新後仕様情報２５０、及び、設計情報２００における変数定義情報２０２及び不変条件情報２０３を記憶装置２０から入手し、構文規則情報（不図示）に基づいて、形式検証を実行可能な形式仕様情報２６０を生成する。構文規則情報は、更新後仕様情報２５０、変数定義情報２０２、及び、不変条件情報２０３を形式仕様のフォーマットに変換可能な規則を示す情報であり、例えば、記憶装置２０に格納されている。
【００５８】
図８は、形式仕様情報２６０の構成を例示する図である。形式仕様情報２６０は、Event-Bにおいてマシンと呼ばれる形式仕様を表す情報である。図８において、形式仕様情報２６０の右側の行番号は説明用の記載であり、この行番号は形式仕様には含まれない。形式仕様情報２６０において、「ＭＡＣＨＩＮＥ」節は、そのマシンの名称を示す。「ＶＡＲＩＡＢＬＥＳ」節は、そのマシンで使用する変数の名称を示す。「ＩＮＶＡＲＩＡＮＴＳ」節は、そのマシンにおいて、各Event-Bイベントの実行前後に成立すべき条件である不変条件を示す。各不変条件の冒頭には「ＩＮＶＡＲＩＡＮＴＳ」節内において一意となるラベルが付与される（例えば「ｉｎｖ１」等）。
【００５９】
「ＥＶＥＮＴＳ」節は、Event-Bイベントを示し、その最後に「ＥＮＤ」が記載される。Event-Bイベントにおいて、冒頭部は、そのEvent-Bイベントの名称を示す。「ＡＮＹ」節は、そのEvent-Bイベントのみで使用する局所変数の名称を示す。「ＷＨＥＲＥ」節は、そのEvent-Bイベントが実行可能となる条件であるEvent-Bガードを示す。Event-Bガードの冒頭には、そのEvent-Bガードが属するEvent-Bイベント内において一意となるラベルが付与される（例えば「ｇｒｄ１」等）。「ＴＨＥＮ」節は、そのEvent-Bイベントが行うEvent-Bアクション（変数への新たな値の代入）を示し、その最後に「ＥＮＤ」が記載される。Event-Bアクションの冒頭には、そのEvent-Bアクションが属するEvent-Bイベント内において一意となるラベルが付与される（例えば「ａｃｔ１」等）。Event-Bイベント「ＩＮＩＴＩＡＬＩＳＡＴＩＯＮ」は変数を初期化するEvent-Bイベントであり、すべてのマシンは、このEvent-Bイベントを定義する必要がある。
【００６０】
変換部１５は、変数定義情報２０２において定義された変数ｘ及びｙを、「ＶＡＲＩＡＢＬＥＳ」節に記載する（図８に示す形式仕様情報２６０の２〜３行目）。変換部１５は、変数定義情報２０２において、変数ｘ及びｙの型がｉｎｔ（整数）であることを「ＩＮＶＡＲＩＡＮＴＳ」節に「ｘ∈ＩＮＴ」「ｙ∈ＩＮＴ」として記載する（形式仕様情報２６０の５〜６行目）。記号「∈」は右辺の集合に左辺の要素が属することを表す。「ＩＮＴ」はEvent-Bにおける整数全体の集合である。変換部１５は、変数定義情報２０２において、変数ｘ及びｙの初期値が順に０と１であることを、「ＩＮＩＴＩＡＬＩＳＡＴＩＯＮ」の「ＴＨＥＮ」節に「ｘ：＝０」、「ｙ：＝１」として記載する（形式仕様情報２６０の１１〜１２行目）。
【００６１】
変換部１５は、不変条件情報２０３において記載された不変条件「ｘ＜ｙ」を、「ＩＮＶＡＲＩＡＮＴＳ」節に記載する（形式仕様情報２６０の７行目）。変換部１５は、図７に示す更新後仕様情報２５０におけるパスｐ１について、Event-Bイベントの名称を「ｐ１」とする（形式仕様情報２６０の１４行目）。変換部１５は、更新後仕様情報２５０における局所変数「ｙ＿１」「ｙ＿２」を「ＡＮＹ」節に記載する（形式仕様情報２６０の１５〜１６行目）。変換部１５は、更新後仕様情報２５０における区分が「ガード」である数式の内容「ｘ＝０」「ｙ＿１＝０」「ｙ＿２＝ｙ＿１＋１」を「ＷＨＥＲＥ」節に記載する（形式仕様情報２６０の１８〜２０行目）。変換部１５は、更新後仕様情報２５０における区分が「アクション」である式の内容「ｙ：＝ｙ＿２」を「ＴＨＥＮ」節に記載する（形式仕様情報２６０の２２行目）。変換部１５は、更新後仕様情報２５０におけるパスｐ２についても、パスｐ１と同様な処理を行う。変換部１５は、生成した形式仕様情報２６０を、記憶装置２０へ格納する。
【００６２】
次に図９乃至１３のフローチャートを参照して、本実施形態に係る形式検証支援装置１０の動作（処理）について詳細に説明する。
【００６３】
図９は、形式検証支援装置１０の動作全体を示すフローチャートである。設計情報処理部１１は、記憶装置２０から、設計情報２００を読み込む（ステップＳ１０１）。設計情報処理部１１は、読み込んだ設計情報２００を基に、ノード情報２１０、及び、フロー情報２２０を生成する（ステップＳ１０２）。パス情報抽出部１２は、設計情報処理部１１により生成されたフロー情報２２０を基に、パス情報２３０を生成する（ステップＳ１０３：詳細は、図１０を参照して後述する）。仕様情報抽出部１３は、設計情報処理部１１により生成されたノード情報２１０及びフロー情報２２０、及び、パス情報抽出部１２により生成されたパス情報２３０を基に、更新前仕様情報２４０を生成する（ステップＳ１０４：詳細は、図１２を参照して後述する）。
【００６４】
更新部１４は、仕様情報抽出部１３により生成された更新前仕様情報２４０を、更新後仕様情報２５０に更新する（ステップＳ１０５：詳細は、図１３Ａ及び図１３Ｂを参照して後述する）。変換部１５は、更新後仕様情報２５０を、構文規則情報に基づいて、形式仕様情報２６０に変換する（ステップＳ１０６）。変換部１５は、生成した形式仕様情報２６０を記憶装置２０へ格納し（ステップＳ１０７）、全体の処理は終了する。
【００６５】
図１０は、形式検証支援装置１０が、図９に示すステップＳ１０３において、パス情報２３０を生成する動作の詳細を示すフローチャートである。パス情報抽出部１２は、空の状態のパス情報２３０を生成する（ステップＳ１００１）。パス情報抽出部１２は、フロー情報２２０において、出力ノードとして未登録であるノードを、起点ノードとして収集する（ステップＳ１００２）。パス情報抽出部１２は、空の一時パスｐを生成する（ステップＳ１００３）。
【００６６】
パス情報抽出部１２は、起点ノードを対象ノードとして、パスを探索する処理を再帰的に行う（ステップＳ１００４：詳細は、図１１を参照して後述する）。パス情報抽出部１２は、当該起点ノードについて、処理済とする（ステップＳ１００５）。未処理である起点ノードが存在する場合（ステップＳ１００６でＹｅｓ）、処理はステップＳ１００３へ戻る。未処理である起点ノードが存在しない場合（ステップＳ１００６でＮｏ）、ステップＳ１０３の処理は終了する。
【００６７】
図１１は、形式検証支援装置１０が、図１０に示すステップＳ１００４において、パス情報２３０を生成する際に、パスの探索を行う動作の詳細を示すフローチャートである。パス情報抽出部１２は、対象ノードを入力ノードとするフローを収集する（ステップＳ１１０１）。パス情報抽出部１２は、処理対象とするフローを、一時パスｐに登録する（ステップＳ１１０２）。
【００６８】
一時パスｐがパス生成条件を満たさない場合（ステップＳ１１０３でＮｏ）、処理はステップＳ１１０７へ進む。一時パスｐがパス生成条件を満たす場合（ステップＳ１１０３でＹｅｓ）、処理はステップＳ１１０４へ進む。当該フローの出力ノードを入力ノードとするフローがある場合（ステップＳ１１０４でＹｅｓ）、パス情報抽出部１２は、当該フローの出力ノードを対象ノードに設定し（ステップＳ１１０６）、処理はステップＳ１１０１へ戻る。当該フローの出力ノードを入力ノードとするフローがない場合（ステップＳ１１０４でＮｏ）、パス情報抽出部１２は、一時パスｐをパス情報２３０に登録し（ステップＳ１１０５）、処理はステップＳ１１０７へ進む。
【００６９】
パス情報抽出部１２は、当該フローを一時パスｐから削除する（ステップＳ１１０７）。当該フローを削除する前の一時パスｐがパス生成条件を満たす場合（ステップＳ１１０８でＹｅｓ）、処理はステップＳ１１１０へ進む。当該フローを削除する前の一時パスｐがパス生成条件を満たさない場合（ステップＳ１１０８でＮｏ）、パス情報抽出部１２は、当該フローを削除した後の一時パスｐをパス情報２３０に登録する（ステップＳ１１０９）。パス情報抽出部１２は、当該フローについて、処理済みとする（ステップＳ１１１０）。未処理であるフローがある場合（ステップＳ１１１１でＹｅｓ）、処理はステップＳ１１０２へ戻る。未処理であるフローがない場合（ステップＳ１１１１でＮｏ）、ステップＳ１００４の処理は終了する。
【００７０】
図１２は、形式検証支援装置１０が、図９に示すステップＳ１０４において、更新前仕様情報２４０を生成する動作の詳細を示すフローチャートである。仕様情報抽出部１３は、空の状態の更新前仕様情報２４０を生成する（ステップＳ１２０１）。仕様情報抽出部１３は、パス情報２３０に登録されているパスのうち、未処理のパスを、処理対象パスとして設定する（ステップＳ１２０２）。仕様情報抽出部１３は、当該パスに含まれる未処理のフローを、処理対象フローとして設定する（ステップＳ１２０３）。
【００７１】
仕様情報抽出部１３は、ノード情報２１０及びフロー情報２２０に基づき、当該フローに含まれるアクションとガードについて、数式区分及び数式の内容を、更新前仕様情報２４０に登録する（ステップＳ１２０４）。仕様情報抽出部１３は、当該フローについて、処理済とする（ステップＳ１２０５）。
【００７２】
未処理であるフローがある場合（ステップＳ１２０６でＹｅｓ）、処理はステップＳ１２０３へ戻る。未処理であるフローがない場合（ステップＳ１２０６でＮｏ）、仕様情報抽出部１３は、当該パスについて、処理済とする（ステップＳ１２０７）。未処理であるパスがある場合（ステップＳ１２０６でＹｅｓ）、処理はステップＳ１２０２へ戻る。未処理であるパスがない場合（ステップＳ１２０６でＮｏ）、ステップＳ１０４の処理は終了する。
【００７３】
図１３Ａ及び図１３Ｂは、形式検証支援装置１０が、図９に示すステップＳ１０５において、更新前仕様情報２４０を更新後仕様情報２５０に更新する動作の詳細を示すフローチャートである。更新部１４は、更新前仕様情報２４０に登録されているパスのうち、未処理のパスを、処理対象パスとして設定する（ステップＳ１３０１）。更新部１４は、更新前仕様情報２４０に登録されている、当該パスにおける数式のうち、未処理の数式を、処理対象数式として設定する（ステップＳ１３０２）。
【００７４】
数式区分がアクションでない（すなわちガードである）場合（ステップＳ１３０３でＮｏ）、更新部１４は、当該数式に含まれる変数について、代入回数情報１４０に値が設定されている場合、当該変数を、その変数名に代入回数情報１４０が示す値を付加した名称を付与した局所変数に置き換える（ステップＳ１３０８）。
【００７５】
数式区分がアクションである場合（ステップＳ１３０３でＹｅｓ）、更新部１４は、当該数式の右辺に含まれる変数について、代入回数情報１４０に値が設定されている場合、当該変数を、その変数名に代入回数情報が示す値を付加した名称を付与した局所変数に置き換える（ステップＳ１３０４）。更新部１４は、当該数式の左辺に含まれる変数について、代入回数情報１４０の値を１加算する（ステップＳ１３０５）。更新部１４は、当該数式の左辺に含まれる変数を、その変数名に代入回数情報１４０が示す値を付加した名称を付与した局所変数に置き換える（ステップＳ１３０６）。更新部１４は、当該数式における代入記号を等号に変更し、数式区分をガードに変更する（ステップＳ１３０７）。
【００７６】
更新部１４は、当該数式について、処理済とする（ステップＳ１３０９）。未処理である数式がある場合（ステップＳ１３１０でＹｅｓ）、処理はステップ１３０２へ戻る。未処理である数式がない場合（ステップＳ１３１０でＮｏ）、更新部１４は、代入回数情報１４０に基づき、局所変数の定義を当該パスに追加する（ステップＳ１３１１）。
【００７７】
更新部１４は、代入回数情報１４０に基づき、変数に最後の局所変数を代入するアクションを当該パスに追加する（ステップＳ１３１２）。更新部１４は、代入回数情報１４０をリセットする（ステップＳ１３１３）。更新部１４は、当該パスについて処理済とする（ステップＳ１３１４）。未処理であるパスがある場合（ステップＳ１３１５でＹｅｓ）、処理はＳ１３０１へ戻る。未処理であるパスがない場合（ステップＳ１３１５でＮｏ）、ステップＳ１０５の処理は終了する。
【００７８】
本実施形態に係る形式検証支援装置１０は、形式手法によってソフトウェアの設計情報に不整合がないことを自動的に検証することを、確実に行うことができる。その理由は、形式検証支援装置１０が、ソフトウェアの設計情報２００から抽出した、変数に対して値を代入する代入処理について、当該変数を代入処理ごとに異なる局所変数に置き換えることによって、局所事後条件が生成されることを回避するからである。
【００７９】
以下に、本実施形態に係る形式検証支援装置１０によって実現される効果について、詳細に説明する。
【００８０】
形式手法では、アクティビティ図におけるノードをEvent-Bイベントと関連付け、ノードが行う処理の結果を局所事後条件を示す論理式により表現することにより、Event-Bによる記述に変換する。この場合、通常、代入式の個数分だけ局所事後条件が生成される。設計情報における整合性を証明する定理証明器は、与えられた不変条件が、元々の設計情報の整合を確認するための条件であるか、あるいは、局所事後条件であるかを判別できない。したがって、ある不変条件がEvent-Bイベントの実行前後で成立することを証明しようとする際に、証明に無関係な多くの局所事後条件の存在が、必要な不変条件を抽出するときに障害となるという問題がある。
【００８１】
これに対して、本実施形態に係る形式検証支援装置１０では、仕様情報抽出部１３は、設計情報２００に含まれる、ソフトウェアが実行を開始してから終了するまでに行う、変数へのアクション（代入処理）ごとの仕様情報を抽出する。更新部１４は、仕様情報抽出部１３によって抽出された各アクションについて、当該変数を、アクションごとに異なる局所変数に置き換える。当該変数が局所変数に置き換えられたアクションは、形式手法において、ガード（後続ノードの実行可否に関する条件を参照する処理）として扱われる。そして更新部１４は、当該変数に関して最後に行われる最終代入処理において置き換えられた前記局所変数の値を当該変数に代入するアクションを追加する内容に、仕様情報を更新する。形式検証支援装置１０が生成した更新後仕様情報２５０は、設計情報２００の論理を維持しており、変数ごとのアクションの数は１つであるので、証明に無関係な多くの局所事後条件が新たに生成されることはない。これにより、本実施形態に係る形式検証支援装置１０は、形式手法によってソフトウェアの設計情報に不整合がないことを自動的に検証することを、確実に行うことができる。
【００８２】
また、形式検証において不整合が見つかった場合に、不整合が発生した処理ステップを特定することはできるが、不整合が発生した情報処理パスを特定することは困難であるという別の問題がある。不整合を起こした原因は、開始ノードから、不整合が発生した処理ステップまでの情報処理パスのどこかに存在するが、その情報処理パスを特定できないと原因を究明することができない。Event-Bでは、複数のEvent-Bイベントについて、それぞれのEvent-Bガードが真となるときに、どのEvent-Bイベントが実行されるかは一意には決まらない。Event-Bガードが真となるEvent-Bイベントのうち、任意の１つのみが非決定的に選択され、そのEvent-Bアクションが、他のEvent-Bイベントからの割り込みなしに実行される。Event-Bイベントをアクティビティ図が示す順序にしたがって実行させるために、例えば特許文献１が示す技術では、ノードの実行順序を制御する変数（実行制御変数）を導入する。不整合が見つかった場合は、不整合が発生したEvent-Bイベントと不整合が発生する条件と実行制御用変数とから、不整合が発生した情報処理パスを見つける必要がある。論理式の集合から目的の情報処理パスを見つけることを、人手作業により行うことは困難である。
【００８３】
この問題に対して、本実施形態に係る形式検証支援装置１０は、パス情報抽出部１２及び仕様情報抽出部１３によって、条件分岐を含む処理を実行するソフトウェアが実行を開始してから終了するまでに行う複数の情報処理パスに関する情報を含む設計情報２００から、それらの複数の情報処理パスに関する仕様情報を抽出する。そして、更新部１４は、情報処理パスごとに、上述した仕様情報を更新する処理を行う。すなわち、本実施形態に係る形式検証支援装置１０は、アクティビティ図における情報処理パスごとにソフトウェアの設計情報の整合性を検証することにより、より効率的な形式検証をおこなうことができる。
【００８４】
なお、本実施形態が示す技術は、Event-Bを用いた形式手法における形式検証に限定されず、Event-B以外の形式手法における形式検証にも適用可能である。
【００８５】
＜第２の実施形態＞
図１４は、第２の実施形態に係る形式検証支援装置３０の構成を概念的に示すブロック図である。
【００８６】
本実施形態に係る形式検証支援装置３０は、抽出部３３、及び、更新部３４を備えている。
【００８７】
抽出部３３は、ソフトウェアが使用する変数に対して値を代入する代入処理に関する情報を含む設計情報から、当該ソフトウェアが実行を開始してから終了するまでに行う代入処理の処理内容を表す仕様情報を抽出する。
【００８８】
更新部３４は、抽出部３３によって抽出された、特定の変数へ値を代入する１以上の代入処理について、その特定の変数を、代入処理同士で互いに（即ち、当該１以上の代入処理間において）異なる新たな変数である局所変数に置き換える。そして、更新部３４は、その特定の変数に関して最後に行われる代入処理である最終代入処理の後に、最終代入処理において置き換えられた局所変数の値をその特定の変数に代入する代入処理を追加する内容に、仕様情報を更新する。
【００８９】
本実施形態に係る形式検証支援装置３０は、形式手法によってソフトウェアの設計情報に不整合がないことを自動的に検証することを、確実に行うことができる。その理由は、形式検証支援装置３０が、ソフトウェアの設計情報から抽出した、変数に対して値を代入する代入処理について、当該変数を代入処理ごとに異なる局所変数に置き換えることによって、局所事後条件が生成されることを回避するからである。
【００９０】
＜ハードウェア構成例＞
上述した各実施形態において図１、及び、図１４に示した各部は、専用のＨＷ（ＨａｒｄＷａｒｅ）（電子回路）によって実現することができる。また、図１及び図１４において、少なくとも、下記構成は、ソフトウェアプログラムの機能（処理）単位（ソフトウェアモジュール）と捉えることができる。
・設計情報処理部１１、
・パス情報抽出部１２、
・仕様情報抽出部１３、
・抽出部３３、
・更新部１４及び３４、
・変換部１５。
【００９１】
但し、これらの図面に示した各部の区分けは、説明の便宜上の構成であり、実装に際しては、様々な構成が想定され得る。この場合のハードウェア環境の一例を、図１５を参照して説明する。
【００９２】
図１５は、本願発明の各実施形態に係る形式検証支援装置を実行可能な情報処理装置９００（コンピュータ）の構成を例示的に説明する図である。即ち、図１５は、図１及び図１４に示した形式検証支援装置を実現可能なコンピュータ（情報処理装置）の構成であって、上述した実施形態における各機能を実現可能なハードウェア環境を表す。
【００９３】
図１５に示した情報処理装置９００は、構成要素として下記を備えている。
・ＣＰＵ（Ｃｅｎｔｒａｌ＿Ｐｒｏｃｅｓｓｉｎｇ＿Ｕｎｉｔ）９０１、
・ＲＯＭ（Ｒｅａｄ＿Ｏｎｌｙ＿Ｍｅｍｏｒｙ）９０２、
・ＲＡＭ（Ｒａｎｄｏｍ＿Ａｃｃｅｓｓ＿Ｍｅｍｏｒｙ）９０３、
・ハードディスク（記憶装置）９０４、
・外部装置との通信インタフェース９０５、
・バス９０６（通信線）、
・ＣＤ−ＲＯＭ（Ｃｏｍｐａｃｔ＿Ｄｉｓｃ＿Ｒｅａｄ＿Ｏｎｌｙ＿Ｍｅｍｏｒｙ）等の記録媒体９０７に格納されたデータを読み書き可能なリーダライタ９０８、
・入出力インタフェース９０９。
【００９４】
即ち、上記構成要素を備える情報処理装置９００は、これらの構成がバス９０６を介して接続された一般的なコンピュータである。情報処理装置９００は、ＣＰＵ９０１を複数備える場合もあれば、マルチコアにより構成されたＣＰＵ９０１を備える場合もある。
【００９５】
そして、上述した実施形態を例に説明した本願発明は、図１５に示した情報処理装置９００に対して、次の機能を実現可能なコンピュータプログラムを供給する。その機能とは、その実施形態の説明において参照したブロック構成図（図１及び図１４）における上述した構成、或いはフローチャート（図９乃至図１３）の機能である。本願発明は、その後、そのコンピュータプログラムを、当該ハードウェアのＣＰＵ９０１に読み出して解釈し実行することによって達成される。また、当該装置内に供給されたコンピュータプログラムは、読み書き可能な揮発性のメモリ（ＲＡＭ９０３）またはハードディスク９０４等の不揮発性の記憶デバイスに格納すれば良い。
【００９６】
また、前記の場合において、当該ハードウェア内へのコンピュータプログラムの供給方法は、現在では一般的な手順を採用することができる。その手順としては、例えば、ＣＤ−ＲＯＭ等の各種記録媒体９０７を介して当該装置内にインストールする方法や、インターネット等の通信回線を介して外部よりダウンロードする方法等がある。そして、このような場合において、本願発明は、係るコンピュータプログラムを構成するコード或いは、そのコードが格納された記録媒体９０７によって構成されると捉えることができる。
【００９７】
以上、上述した実施形態を模範的な例として本願発明を説明した。しかしながら、本願発明は、上述した実施形態には限定されない。即ち、本願発明は、本願発明のスコープ内において、当業者が理解し得る様々な態様を適用することができる。
【符号の説明】
【００９８】
１０    形式検証支援装置
１１    設計情報処理部
１２    パス情報抽出部
１３    仕様情報抽出部
１４    更新部
１４０    代入回数情報
１５    変換部
２０    記憶装置
２００    設計情報
２０１    アクティビティ情報
２０１０    開始ノード
２０１１    ディシジョンノード
２０１２    アクションノード
２０１３    アクションノード
２０１４    マージノード
２０１５    アクションノード
２０１６    終了ノード
２０２    変数定義情報
２０３    不変条件情報
２１０    ノード情報
２２０    フロー情報
２３０    パス情報
２４０    更新前仕様情報
２５０    更新後仕様情報
２６０    形式仕様情報
３０    形式検証支援装置
３３    抽出部
３４    更新部
９００    情報処理装置
９０１    ＣＰＵ
９０２    ＲＯＭ
９０３    ＲＡＭ
９０４    ハードディスク（記憶装置）
９０５    通信インタフェース
９０６    バス
９０７    記録媒体
９０８    リーダライタ
９０９    入出力インタフェース
【図１】
2017107347.tif 000003
【図２】
2017107347.tif 000004
【図３】
2017107347.tif 000005
【図４】
2017107347.tif 000006
【図５】
2017107347.tif 000007
【図６】
2017107347.tif 000008
【図７】
2017107347.tif 000009
【図８】
2017107347.tif 000010
【図９】
2017107347.tif 000011
【図１０】
2017107347.tif 000012
【図１１】
2017107347.tif 000013
【図１２】
2017107347.tif 000014
【図１３Ａ】
2017107347.tif 000015
【図１３Ｂ】
2017107347.tif 000016
【図１４】
2017107347.tif 000017
【図１５】
2017107347.tif 000018