(57)【要約】【課題】ソフトウエアの設計情報からモデル検査用の「検証用性質」を自動生成し、設計情報に付与された時間制約を自動で検証用性質に追加し、抽象度(階層)を意識する必要なく、データ送受信シーケンス及び時間制約を用意できるようにする。【解決手段】本発明はモデル検査支援装置として提案される。このモデル検査支援装置は、１階層以上のＤＦＤに基づいて作成されたデータ送受信シーケンスに基づいて、データ送受信シーケンスに記述された個々のプロセス間で送受信されるデータを上記シーケンス通りに仲介するプロセスを検証用追加モデルとして生成する追加モデル生成部と、前記検証用追加モデルに基づいて、当該プロセスが最後まで停止することなく到達することを調査する検証式を生成する検証式作成部とを有する。【選択図】図１
2010026704.tif 000002
【特許請求の範囲】
【請求項１】
１階層以上の階層を有するデータフローダイアグラムの各階層のプロセス間で送受信されるデータである送受信データ及びこの送受信データが送受信される順番を記述したデータであるデータ送受信シーケンスとを入力データとして受け取り、前記送受信データの送信及び受信に対応する遷移を追加することにより作成されるプロセスを検証用追加モデルとして生成する追加モデル生成手段と、
前記検証用追加モデルに基づいて、検証対象であるモデルに相当するプロセスが最後まで停止することなく到達することを調査する検証式を生成する検証式作成手段と
を有することを特徴とするモデル検査支援装置。
【請求項２】
予め用意された検証用モデルを入力として受け取り、前記検証用モデルにおけるデータ受信処理を、データの送信発生を確認後受信する処理に修正することにより、修正された検証用モデルを生成する検証用モデル修正手段をさらに有することを特徴とする、請求項１に記載のモデル検査支援装置。
【請求項３】
前記検証用追加モデル生成手段は、各階層のデータフローダイアグラムに対応するデータ送受信シーケンスごとに、その階層における送受信データのみに基づいて作成されたプロセスである検証用追加モデルを生成することを特徴とする、請求項１又は２に記載のモデル検査支援装置。
【請求項４】
前記検証用追加モデル生成手段は、前記データ送受信シーケンスが、並行して行われる複数の動作である並行動作を含む場合に、それぞれの動作について検証用追加モデルを生成することを特徴とする、請求項１から３のいずれかに記載のモデル検査支援装置。
【請求項５】
前記データ送受信シーケンスに記述された複数のデータの送信と受信の間に対して規定された時間制約を入力として受け取り、前記検証用追加モデル生成手段が生成した検証用追加モデルに、データの送受信にかかる時間経過が前記時間制約を満たすかどうかを判定する遷移を追加する時間制約反映手段をさらに有することを特徴とする、請求項１から４のいずれかに記載のモデル検査支援装置。
【請求項６】
同一階層に属する複数のデータフローダイアグラムに対応する複数のデータ送受信シーケンスに基づいて生成された検証用追加モデルについて、これら検証用追加モデルの初期状態と最終状態をそれぞれ一つに併合して新たな検証用追加モデルを生成する複数シナリオ併合手段をさらに有することを特徴とする、請求項１から５のいずれかに記載のモデル検査支援装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査支援装置に関し、より詳しくはモデル検査器の入力を生成するためのモデル検査支援装置に関する。
【背景技術】
【０００２】
近年のコンピュータを利用したさまざまな装置の普及発展に伴い、これら装置の制御を司るソフトウエア、プログラムの開発も盛んになってきている。これに伴って、これらソフトウエアプログラムが適正に動作するか否かを検査するための技術として、モデル検査技術が提案されるようになってきた（例えば、非特許文献１）。
【０００３】
並行に動作する複数のプロセスを対象としたモデル検査では、個々のプロセスの振る舞いや処理フローを表現する「検証用モデル」と、システムとして望ましい振る舞いや発生しては困る性質を表現する「検証用性質」の2種類を記述する必要がある。
【０００４】
また、上流設計の手法に一つに、プロセスの単位となるコンポーネントを階層的に分割し、コンポーネント間のデータ送受信関係を定義するデータフローダイアグラム（以下、ＤＦＤ）や、ＤＦＤに準じていくつかのシステム利用シナリオにおけるデータ送受信シーケンスを設計情報として作成する手法がある。
【非特許文献１】UPPSALA UNIVERSITY、AALBORG UNIVERSITY、  ”UPPAAL”、  [online] [平成２０年６月３０日検索]、インターネット  <URL:http://www.uppaal.com>
【発明の開示】
【発明が解決しようとする課題】
【０００５】
上記のモデル検査を実行する場合、検証用モデルはプロセスの処理フローを記述した状態遷移表や状態遷移図を基に記述することが比較的容易であるが、「検証用性質」のそれぞれの項目である「検証項目」の記述は、基にすべき設計情報が少なく困難であった。一般には自然言語で書かれたシステムの要求仕様や機能要求を基に、「検証用性質」のそれぞれの項目である「検証項目」を記述するが、特に自然言語からの作成は難しく、検証用性質をいかに多く用意できるかがモデル検査を行う上でのポイントの一つとなっている。
【０００６】
本発明は、これらの設計情報から「検証用性質」を自動生成することを目的とする。
【０００７】
また、大規模リアルタイムシステムの設計手法の一つとして、時間制約を階層的に分割していく手法が考えられている。その場合、階層的に分割していくＤＦＤに準じたデータ送受信シーケンスに時間制約を付加していくことが自然である。本発明は、設計情報に付与された時間制約を自動で検証用性質に追加することを目的とする。
【０００８】
また、上記モデル検査を行う場合には、一般に「検証用モデル」と「検証用性質」の抽象度を合わせる必要があった。具体的には、検証用モデルとして内部の処理フローを記述した個々のプロセスの階層を統一するとともに、検証用性質も検証用モデルの階層に対応させる必要があったが、人手によりこの対応を計ることは困難であったり、限られた時間内で行うには難しいという問題があった。本発明の３番目の目的は、異なる階層のＤＦＤや、それぞれのＤＦＤに準じたシナリオ毎のデータ送受信シーケンス及び時間制約を用意し、かつ、異なる階層のプロセスの内部処理フローに対応する検証用モデルを用意したとしても、個々のプロセスと同一及び上位の階層のＤＦＤと上位の階層のＤＦＤに準じたシナリオ毎のデータ送受信シーケンス及び時間制約が当該プロセスに対応する検証用性質となり、抽象度(階層)を意識する必要をなくすることにある。
【課題を解決するための手段】
【０００９】
上記課題を解決するための手段として、本発明配下の特徴を有する。  
本発明はモデル検査支援装置として提案される。このモデル検査支援装置は、  １階層以上の階層を有するデータフローダイアグラムの各階層のプロセス間で送受信されるデータである送受信データ及びこの送受信データが送受信される順番を記述したデータであるデータ送受信シーケンスとを入力データとして受け取り、前記送受信データの送信及び受信に対応する遷移を追加することにより作成されるプロセスを検証用追加モデルとして生成する追加モデル生成手段と、前記検証用追加モデルに基づいて、検証対象であるモデルに相当するプロセスが最後まで停止することなく到達することを調査する検証式を生成する検証式作成手段とを有することを特徴としている
【発明の効果】
【００１０】
本発明によれば、モデル検査の検証用性質を通常作成している設計情報から容易に作成することが可能となる。
【００１１】
また、本発明の別の態様によれば、設計情報に付与された時間制約を、自動的に検証用性質に追加することが可能となる。
【００１２】
また、本発明のさらに別の態様によれば、モデル検査に使用する「検証用モデル」と「検証用性質」の抽象度を意識することなく、「検証用モデル」と「検証用性質」の作成を可能とする。
【発明を実施するための最良の形態】
【００１３】
以下、図面を参照しながら本発明の実施の形態を説明する。  
本発明の実施の形態は、モデル検査支援装置として提案される。このモデル検査支援装置は、モデル検査ツール（モデル検査器ともいう。一例としてＵＰＰＡＡＬ、ＳＭＶ、ＳＰＩＮ）にモデル検査を実行させるための検証用モデル及び検証用性質を生成する装置である。
【００１４】
［１．モデル検査支援装置の構成例］
モデル検査支援装置は、例えばコンピュータ、ワークステーションなどの情報処理装置によって実現される装置である。この情報処理装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、入出力装置（Ｉ／Ｏ）、及び必要な場合にはハードディスク装置等の外部記憶装置を具備している装置である。モデル検査支援装置は、前記ＲＯＭ、もしくは外部記憶装置などに情報処理装置をモデル検査支援装置として機能させるためのプログラム、もしくはモデル検査支援方法をコンピュータに実行させるためのプログラムが記憶されており、該プログラムを主メモリ上に載せ、ＣＰＵがこれを実行することによりモデル検査支援装置又はモデル検査支援方法が実現される。また、上記プログラムは必ずしも当該装置内の記憶装置に記憶されていなくともよく、磁気ディスク、光ディスク、光磁気ディスク、ＣＤ（Compact Disc）、ＤＶＤ（Digital Video Disc）などのコンピュータ読み取り可能なプログラム記録媒体や、外部の装置（例えば、ＡＳＰ（アプリケーション・サービス・プロバイダ）のサーバなど）から提供され、これを主メモリに乗せる構成であってもよい。
【００１５】
図１は、本実施の形態にかかるモデル検査支援装置の構成例を示した機能ブロック図である。
モデル検査支援装置１は、追加モデル生成手段である追加モデル生成部２２と，追加モデル生成部２２に接続された検証モデル修正部２１（本発明の検証モデル修正手段に相当する）と、追加モデル生成部２２に接続された時間制約反映部２３（本発明の時間制約反映手段に相当する）と、時間制約反映部２３に接続された複数シナリオ併合部２４（本発明の複数シナリオ併合手段に相当する）と、複数シナリオ併合部２４に接続された検証式作成部２５（本発明の検証式作成手段に相当する）とを有している。なお、ここにいう「接続される」とは、データの受け渡しが行われれば足りる関係を示しており、物理的に接続されることに限定されていない。
【００１６】
モデル検査支援装置１は、入力データとして、検証用モデル１１，データ送受信シーケンス１２，及び時間制約１３を用いる。これらの入力データは、予め利用者が用意しておくものである。入力された検証用モデル１１は検証モデル修正部２１に渡される。データ送受信シーケンス１２は追加モデル生成部２２に渡され、及び時間制約１３は時間制約反映部２３に渡される。
【００１７】
モデル検査支援装置１は、その出力データとして、修正済み検証用モデル３１，追加分検証用モデル３２，及び検証式３３を出力する。これら出力データである修正済み検証用モデル３１，追加分検証用モデル３２，及び検証式３３は、モデル検査器４０（「モデル検査ツール」ともいう）の入力データとなる。これら修正済み検証用モデル３１，追加分検証用モデル３２，及び検証式３３を与えられたモデル検査器４０は、検査結果４１を出力する。
【００１８】
［１．モデル検査支援装置への入力データ］
次に、モデル検査支援装置１への入力データである検証用モデル１１，データ送受信シーケンス１２，及び時間制約１３について説明する。
【００１９】
本モデル検査支援装置１，並びにその出力データを利用するモデル検査器４０が検査対象とするものは、ソフトウエア（一部のみでもよい）である。
実施例で用いる、検証対象のソフトウエア（「検査対象ソフトウエア」と呼ぶ）の設計情報を図２〜図６の図を用いて説明する。利用者はモデル検査支援装置１及びモデル検査器４０を用いて、この検査対象ソフトウエアについての検査結果４１を求めることを目的としている。利用者は検査結果４１を参照することにより、検査対象ソフトウエアに問題がないか否かを知ることができ、問題がある場合にはその問題を解決するよう検査対象ソフトウエアの修正を行うことができる。
【００２０】
［１．１．最上位階層（レベル１）］
図２は、検証対象のソフトウエアの最上位階層（レベル１ともいう）のＤＦＤと、このＤＦＤに準じたシナリオのデータ送受信シーケンスを示している。図２において、矩形枠で示した部分はソフトウエア全体２００を意味し、円形枠で示した「ＰＡ」及び「ＰＢ」はそれぞれ検査対象ソフトウエアの最上位のコンポーネント２０１を意味している。コンポーネントとは、プログラム中で、あるまとまりを持ち、他のコンポーネントとデータの送受信を行いながら処理を進める構成要素をいう。コンポーネント２０１に入る矢印とコンポーネントから出て行く矢印はそれぞれコンポーネントが受信するデータ、コンポーネントが送信するデータを意味する。矢印に付与した記号「Ｘ」、「Ｙ」、「Ｚ」はデータ名を示すものとする。
【００２１】
図２に示したＤＦＤでは、左側のコンポーネントＰＡはデータＸを受信し、データＹを送信することを意味する。
また、図中、丸数字（丸で囲まれた数字）はデータ送受信シーケンス（送受信が行われる順番）を意味するものとする。図２に示したＤＦＤでは、コンポーネントＰＡがデータＸを受信した（丸数字１）後に、コンポーネントＰＡがデータＹを送信し（丸数字２）、このデータＹをコンポーネントＰＢが受信した（丸数字２）後、コンポーネントＰＢはデータＺを送信する（丸数字３）ことを意味する。なお、データＹに関する矢印はコンポーネントＰＡから出てコンポーネントＰＢに入っており、これはコンポーネントＰＡがデータＹを送信したと同時にコンポーネントＰＢがデータＹを受信したことを意味しており、以降では、このような状態を示す矢印を単に「データＹが送受信された」とも呼ぶこともある。
【００２２】
また、図２には、の最上位階層についての時間制約１３の内容として時間制約３０１が記載されている。この時間制約３０１において、上段式「Ｘ〜Ｙ＜１５０」は、データＸがコンポーネントＰＡにより受信されてから、データＹが送受信されるまでの時間が１５０未満（単位は任意、例えばミリ秒、以下同じ）であることを意味している。同様に、下段式「Ｙ〜Ｚ＜１００」は、データＹがコンポーネントＰＢに受信されてから、データＺが送受信されるまでの時間が１００未満であることを意味している。
【００２３】
図２に示す様な、最上位階層のＤＦＤとこのＤＦＤに準じたシナリオのデータ送受信シーケンスは、例えば図７に示すデータ形式で記述されてデータ化される。データ化された最上位階層のＤＦＤとこのＤＦＤに準じたシナリオのデータ送受信シーケンスは、モデル検査支援装置１に入力される。また、このシナリオの時間制約３０１は、例えば、図８に示すようなデータ形式で記述され、システムに入力されるとする。なお、図７、図８に示すデータ形式は本発明で用いられるデータ形式の一例であって、本発明がこのようなデータ形式を用いるものに限定される趣旨ではない。
【００２４】
［１．２．下位階層（レベル２）］
次に、上記最上位階層の一つ下の階層のＤＦＤとこのＤＦＤに準じたシナリオのデータ送受信シーケンス、及びその時間制約について説明する。
【００２５】
階層化設計により、最上位階層である上記コンポーネントＰＡは、図３に示すように、４つの下位コンポーネントＰ１、Ｐ２、Ｐ３、Ｐ４に分割されるものとしよう。なお、最上位階層のコンポーネントＰＡ，ＰＢから分割された下位コンポーネント群はレベル２の階層に属するとする。
【００２６】
図３は、コンポーネントＰＡに相当する、レベル２の下位コンポーネントについてのＤＦＤとこのＤＦＤに準じたシナリオのデータ送受信シーケンスを示す図である。一方、レベル２では、図３の他にも図４に示すシナリオも存在するとする。すなわち、コンポーネントＰＡは、ある条件に基づいて２つの異なるシナリオに従って動作する。
【００２７】
両シナリオを区別するため、図３に示したシナリオを「シナリオ１」、図４のシナリオを「シナリオ２」と呼んで区別することにする。以下、シナリオ１及びシナリオ２について説明する。本モデル検査支援装置１の利用者は、複数のシナリオが存在する場合にはそれぞれのシナリオについて、ＤＦＤ及びそのＤＦＤに準ずるデータ送受信シーケンス、時間制約を準備する必要がある。
【００２８】
［１．２．１．シナリオ１のＤＦＤ、データ送信シーケンス、及び時間制約］
図３に示すシナリオ１のＤＦＤ及びそのＤＦＤに準ずるデータ送受信シーケンスでは、下位コンポーネント（参照符号２０２）Ｐ１，Ｐ２，Ｐ３、Ｐ４が存在する。
【００２９】
シナリオ１では、データＸが下位コンポーネントＰ１に受信された後（丸数字１）、データａが下位コンポーネントＰ１から下位コンポーネントＰ２に送受信される（丸数字２）。その後データｂが下位コンポーネントＰ２から下位コンポーネントＰ３に送受信される（丸数字３）とともに、データｅが下位コンポーネントＰ２から下位コンポーネントＰ４に送受信される（丸数字３）。ここで、データｂの送受信とデータｃの送受信の順番は特に規定されていないとする。データbの送受信の後、データcが下位コンポーネントＰ３から下位コンポーネントＰ１に送受信される（丸数字４）。その後、データdが下位コンポーネントＰ１から下位コンポーネントＰ４に送受信される（丸数字５）。その後データＹが下位コンポーネントＰ４から送信される（丸数字６）ことを意味している。
【００３０】
また、このシナリオ1においては、時間制約として、データaの送受信からデータbの送受信までの時間が30未満、同様にデータaからデータbは100未満、データcからデータdは20未満とする（図３、時間制約３０２参照）。図５に、図３に示すシナリオ１におけるデータの送受信の順番関係を示す。以上のＤＦＤとこのＤＦＤに準じたシナリオのデータ送受信シーケンスは、図９に示すデータ形式で記述され、モデル検査支援装置１に入力される。また、このシナリオ１の時間制約１３である時間制約３０２は、図１０に示すデータ形式で記述され、モデル検査支援装置１に入力される。
【００３１】
［１．２．２．シナリオ２のＤＦＤ、データ送信シーケンス、及び時間制約］
次に、コンポーネントＰＡの別のシナリオ、すなわちシナリオ２のＤＦＤ及びデータ送信シーケンスを図４に示す。なお、シナリオ２では下位コンポーネントＰ３はデータの送受信を行わないので図示しない。
【００３２】
図４のシナリオ2のデータ送受信シーケンスでは、データＸが下位コンポーネントＰ１に受信された（丸数字１）後、データａが下位コンポーネントＰ１から下位コンポーネントＰ２に送受信される（丸数字２）とともに、データｄが下位コンポーネントＰ１から下位コンポーネントＰ４に送受信される（丸数字２）。ここで、データａの送受信とデータbの送受信の順番は特に規定されていないとする。データａの送受信の後、データｅが下位コンポーネントＰ２から下位コンポーネントＰ４に送受信される（丸数字３）。その後データＹが下位コンポーネントＰ４から送信される（丸数字４）ことを意味している。
【００３３】
図４に示したデータ送信シーケンスについて、図６にそのデータの送受信の順番関係を示す。
図４及び図６に示すようなＤＦＤとこのＤＦＤに準じたシナリオのデータ送受信シーケンス１２は、図１１に示すデータ形式で記述され、モデル検査支援装置１に入力される。
なお、シナリオ２においては、時間制約１３は存在しないとする。従って、シナリオ１における時間制約３０２や、図９に示した時間制約のデータもシナリオ２においては準備する必要はない。
【００３４】
［１．２．３．入力用の検証用モデル］
上述のデータ送受信シーケンス１２及び時間制約１３に加えて、利用者はモデル検査支援装置１の入力として、検証用モデル１１を用意する必要がある。以下、図２，３，４に示したＤＦＤに対応する検証用モデル１１について説明する。
【００３５】
この実施の形態では、コンポーネントＰＡの下位コンポーネントＰ１、Ｐ２、Ｐ３、Ｐ４のそれぞれ、及びコンポーネントＰＤについて、各プロセスの内部フローを表現するモデル検査のための検証用モデル１１を用意する。検証用モデル１１は、モデル検査器４０が受け付けるデータ形式であればどのようなものでもかまわない。ここでは、モデル検査器４０がＵＰＰＡＡＡＬ（http://www.uppaal.com  参照）である場合の例として説明するが、本発明がこのような検証モデルに限定される趣旨ではない。
【００３６】
検証用モデル１１として下位コンポーネントＰ１の検証用モデルを図１２に、下位コンポーネントＰ２の検証用モデルを図１３に、下位コンポーネントＰ３の検証用モデルを図１４に、下位コンポーネントＰ４の検証用モデルを図１５に、コンポーネントＰＢの検証用モデルを図１６に示す。
【００３７】
さらに、検査対象ソフトウエア２００に対する、入出力データを生成するシステム外の環境envの処理フローを表現する検証モデルを図１７に示す。
【００３８】
これら図１２から図１７までに示された検証用モデルがモデル検査支援装置１の入力データである検証用モデル１１として使用される。
【００３９】
［２．モデル検証支援装置の動作］
次に、女出る検証支援装置１の動作例について説明する。なお、ここでの動作例の説明は上述の入力データである検証用モデル１１，データ送受信シーケンス１２，時間制約１３が入力された場合を例として説明する。
【００４０】
［２．１．追加モデル生成処理］
まず、追加モデル生成部２２が実行する追加モデル生成処理について説明する。図１８は、追加モデル生成部２２が実行する追加モデル生成処理の例を示すフローチャートである。以下、図１８を参照しながら追加モデル生成処理の例を説明する。
【００４１】
データ送受信シーケンスを入力された追加モデル生成部２２は、まずそのデータ送受信シーケンスに付されたシナリオ名を名称とする検証モデルプロセスを追加する（Ｓ１８０１）。次に、追加モデル生成部２２は、そのデータ送受信シーケンスにおける送受信データ毎に送信発生を示すフラグ宣言を追加する（Ｓ１８０２）。次に、追加モデル生成部２２は、初期ロケーションを追加し、そのシナリオに含まれるデータ送受信に従い後述のＳ１８０４、Ｓ１８０５の処理を行う（Ｓ１８０３）。すなわち、追加モデル生成部２２は、次のデータ送受信がＤＦＤの外部コンポーネントとの入出力で、かつ、このＤＦＤが最上位階層でないかどうかを判定する（Ｓ１８０４）。この条件を満たしている場合（Ｓ１８０４，Ｙｅｓ）、追加モデル生成部２２はデータ送受信シーケンスに含まれる全データ送受信に対して、Ｓ１８０４，Ｓ１８０５を実行したか否かを判定する（Ｓ１８０６）。全データ送受信に対して実行済みであれば（Ｓ１８０６，Ｙｅｓ）、後述するＳ１８０７に進む。一方、全データ送受信に対して実行済みでない場合（Ｓ１８０６，Ｎｏ）、追加モデル生成部２２はＳ１８０４に戻る。
【００４２】
Ｓ１８０４の説明に戻る。Ｓ１８０４において前述の所定条件が満たされていないと判定した場合（Ｓ１８０４，Ｎｏ）、追加モデル生成部２２はそのデータ送受信に対して以下の２遷移を追加する。
【００４３】
（１）「guard」を”データが未送信”とし、「sync」を”当該データの受信”とし、「update」を”当該データのフラグを送信済み”にする遷移
（２）「guard」を”なし”とし、「sync」を”当該データの送信”とし、「update」を”当該データのフラグを未送信”にする遷移
上記の２遷移を追加した後、追加モデル生成部２２はステップＳ１８０６に進む。
【００４４】
ステップＳ１８０６において、全データ送受信に対して実行済みであると判定した場合（Ｓ１８０６，Ｙｅｓ）、追加モデル生成部２２は、この検証モデルプロセスに、シナリオ終了を示すロケーションを追加して、当該ロケーションに”fin”という名称を付与する（Ｓ１８０７）。
以上で、追加モデル生成部２２が実行する追加モデル生成処理が終了する。
【００４５】
［２．１．１．複数シナリオがある場合の追加モデル生成処理］
上記の追加モデル生成処理は、シナリオが一つである場合の処理例であり、図３，図４に示したように複数のシナリオが存在する場合には、追加モデル生成部２２が実行する追加モデル生成処理は以下のように行われる。図１９Ａ及び図１９Ｂに、複数のシナリオが存在する場合の追加モデル生成処理のフローチャートを示す。なお、図１９Ｂは図１９Ａにおける分岐Ａ，Ｂに続くフローチャートである。
【００４６】
図１９Ａにおいて、ステップＳ１９０１からＳ１９０７は、図１８のステップＳ１８０１からＳ１８０７と同様であるので、ここでは、ステップＳ１９０１からＳ１９０７の内容の説明は省略する。
【００４７】
図１９Ａ，ステップＳ１９０５を終了すると、追加モデル生成部２２は、図１９Ｂ、ステップＳ１９０８に進む。ステップＳ１９０８において、追加モデル生成部２２は、次のデータ送受信が並行する複数のデータ送受信であるか否かを判定する（Ｓ１９０８）。次のデータ送受信が並行する複数のデータ送受信でないと判定した場合（Ｓ１９０８，Ｎｏ）、
追加モデル生成部２２は、ステップＳ１９０６（図１９Ａ参照）に直ちに進む。
【００４８】
一方、Ｓ１９０８の判定において、次のデータ送受信が並行する複数のデータ送受信であると判定した場合（Ｓ１９０８，Ｙｅｓ）、追加モデル生成部２２は、次のデータ送受信を起点として、並行して進行する複数シナリオの中のマージ点までを、それぞれサブシナリオとして抽出する（Ｓ１９０９）。
【００４９】
次に、追加モデル生成部２２は、各サブシナリオの先頭に、当該サブシナリオ開始を意味するデータ受信を追加する（Ｓ１９１０）。次に、追加モデル生成部２２は、サブシナリオの最後に当該サブシナリオ完了を意味するデータ送信を追加する（Ｓ１９１１）。次に、追加モデル生成部２２は、各サブシナリオに相当する検証モデルプロセスを、本フローに従い別途作成する（Ｓ１９１２）。次に、追加モデル生成部２２は、本検証モデルプロセスに以下の遷移を、作成したサブプロセス分追加する（Ｓ１９１３）。
【００５０】
（１）「guard」を”なし”とし、「sync」を”サブブロセス開始のデータ送信”とし、「update」を”なし”とする遷移
次に、追加モデル生成部２２は、マージ点のデータ送受信を次のデータ送受信とする（Ｓ１９１４）。このステップＳ１９１４の後、図１９ＡのステップＳ１９０６に進み、次に前述のステップＳ１９０７を実行して、追加モデル生成処理を終了する。
【００５１】
上記の処理の具体例をさらに説明する。まず、最上位階層のＤＦＤのシナリオのデータ送受信シーケンス１２として、図７に示したデータが追加モデル生成部２２に入力されたものとする。追加モデル生成部２２は、この入力データに対して図１９Ａ，図１９Ｂに示した追加モデル生成処理を実行すると、図２４に示す検証用追加モデルを生成する。
上記最上位階層の下位の階層、すなわちレベル２のＤＦＤのデータ送受信シーケンス１についても、同様に検証用追加モデルを生成する。
【００５２】
レベル２のＤＦＤのシナリオ1のデータ送受信シーケンス１２である、図９に示すデータが入力されると、追加モデル生成部２２は、図１９Ａ，Ｂに示す追加モデル生成処理に従い、図２５，図２６，図２７に示す検証用モデルを生成する。ここで、図２６に示す検証用追加モデルと、図２７に示す検証用追加モデルは、前述のシナリオ１（図３，図５参照）において並行的に動作する処理を、サブプロセスとして別途生成したものである。これら３つの検証用モデルを追加することで、図９に示した、レベル２のＤＦＤのシナリオ１のデータ送受信シーケンス１２に対する検証が可能となる。
【００５３】
前述のレベル２のＤＦＤのシナリオ２のデータ送受信シーケンス１２である、図１１に示すデータが入力されると、追加モデル生成部２２は図１９Ａ，Ｂに示す追加モデル生成処理を実行し、図２８，図２９，図３０に示す検証用モデルを生成する。ここで、図２９に示す検証用追加モデルと、図３０に示す検証用追加モデルは、前述のシナリオ２（図４，図６参照）において並行的に動作する処理を、サブプロセスとして別途生成したものである。これら３つの検証用モデルを追加することで、図１１に示した、レベル２のＤＦＤのシナリオ２のデータ送受信シーケンス１２に対する検証が可能となる。
【００５４】
［２．２．時間制約反映部の動作例；時間制約反映処理］
次に、時間制約反映部２３の動作例を説明する。時間制約反映部２３は、時間制約１３と、追加モデル生成部２２が生成した検証用追加モデルを入力として、時間制約反映処理を実行し、実行結果として検証用モデルを出力する。
【００５５】
図２０に時間制約反映処理の一例であるフローチャートを示す。この時間制約反映処理において、時間制約反映部２３は、まず時間制約ごとに時間変数の宣言を追加する（Ｓ２００１）。次に、時間制約反映部２３は、時間制約ごとに下の処理を行う（Ｓ２００２）。すなわち、その時間制約の起点となる遷移の「update」に当該時間制約に対応する時間変数のクリアを追加する（Ｓ２００３）。次に、時間制約反映部２３は、その時間制約の評価点となる遷移の後ろ（次）にcommittedロケーション（円内に文字Ｃを配置して表記する）を追加するとともに、以下の２遷移をor形式で挿入する（Ｓ２００４）。
【００５６】
（１）「guard」を”時間制約”とし、「sync」を”なし”とし、「update」を”なし”とする遷移
（２）「guard」を”時間制約の否定”とし、「sync」を”なし”とし、「update」を”flag:=true”とする遷移
次に、時間制約反映部２３は全時間制約に対して、上記Ｓ２００３，Ｓ２００４の処理を実行したか否かを判定する（Ｓ２００５）。全時間制約に対して実行していないと判定した場合（Ｓ２００５，Ｎｏ）、時間制約反映部２３はステップＳ２００３に戻って、処理を続行する。一方、全時間制約に対して実行したと判定した場合（Ｓ２００５，Ｙｅｓ）、時間制約反映部２３は時間制約反映処理を終了する。
【００５７】
この時間制約反映部２３による時間制約反映処理の具体例を説明する。時間制約反映部２３は、図８に示す最上位階層のＤＦＤのシナリオの時間制約１３の入力データと、図２４に示す検証用追加モデル（追加モデル生成部２２によって出力されている）とを入力として受け取り、これらについて図２０に示す時間制約反映処理を実行し、その結果として図３１に示す検証用追加モデルを出力する。
【００５８】
また、時間制約反映部２３は、図１０に示すレベル2のＤＦＤのシナリオ1の時間制約１３と、図２５に示す検証用追加モデル（追加モデル生成部２２によって出力されている）を入力として受け取り、これらについて図２０に示す時間制約反映処理を実行し、その結果として図３２に示す検証用追加モデルを出力する。
【００５９】
さらに、時間制約反映部２３は、図１０に示すレベル2のＤＦＤのシナリオ1の時間制約１３と、図２６に示す検証用追加モデル（追加モデル生成部２２によって出力されている）を入力として受け取り、これらについて図２０に示す時間制約反映処理を実行し、図３３に示す検証用モデルを出力する。
【００６０】
一方、時間制約反映部２３は、図１０とに示すレベル2のＤＦＤのシナリオ1の時間制約１３と、図２７に示す検証用追加モデル（追加モデル生成部２２によって出力されている）を入力として受け取り、これらについて図２０に示す時間制約反映処理を実行するが、図２７に示す当該検証用追加モデルの範囲に時間制約に係わる部分が含まれないため、出力される検証用追加モデルは、図２７にしめすものと同値のものを出力する。そのため、本明細書においては、時間制約反映部２３がこの場合に出力する検証用追加モデルの図は省略した。
【００６１】
また、レベル２のＤＦＤのシナリオ２（図４，図６参照）に関しては、時間制約が与えられていないため、追加モデル生成部２２によって出力されている図２８、図２９、図３０に示した検証用追加モデルは、時間制約反映部２３において変更は加えられず、そのまま出力される。
【００６２】
ここで、時間制約反映部による処理を経た時点での検証用モデルを整理すると、図31、図32、図33、図27、図28、図29、図30となる。
【００６３】
［２．３．複数シナリオ併合部の動作例；複数シナリオ併合処理］
次に複数シナリオ併合部２４の動作を説明する。複数シナリオ併合部２４は、時間制約反映部２３から出力される検証用追加モデルのうち、並行動作の結果生成されたサブプロセスに対応する検証用追加モデル以外の検証用追加モデルから、複数シナリオを併合した検証用追加モデルを生成する。
【００６４】
図２１は、複数シナリオ併合部２４によって実行される複数シナリオ併合処理の一例を示したフローチャートである。
複数シナリオ併合処理において、複数シナリオ併合部２４は、まず入力された検証用追加モデルについて、該当する階層名を名称とする検証モデルプロセスを追加する（Ｓ２１０１）。次に、複数シナリオ併合部２４は、追加した検証モデルプロセスにおいて、初期ロケーションと、シナリオ完了を意味する"fin"という名称の最終ロケーションを追加する（Ｓ２１０２）。続いて、複数シナリオ併合部２４は、該当する階層に属する各シナリオに関して、以下の処理（Ｓ２１０４，Ｓ２１０５）を行う（Ｓ２１０３）。すなわち、複数シナリオ併合部２４は、まず該当するシナリオに対応する検証モデルプロセス（検証用追加モデル）の初期ロケーションを削除して、当該階層の検証モデルプロセスの初期ロケーションと接続し、その遷移guardを、当該シナリオであることを示す条件とする（Ｓ２１０４）。次に、複数シナリオ併合部２４は、そのシナリオに対応する検証モデルプロセス（検証用追加モデル）の最終ロケーションを削除して、該階層の検証モデルプロセスの最終ロケーションと接続する（Ｓ２１０５）。
【００６５】
次に、複数シナリオ併合部２４は、入力された検証用追加モデルに関し、全階層の全シナリオについてステップＳ２１０４、Ｓ２１０５を実行したか否かを判定する（Ｓ２１０６）。上記条件を満たしていると判定した場合（Ｓ２１０６，Ｙｅｓ）、複数シナリオ併合部２４は複数シナリオ併合処理を終了する。一方、上記条件を満たしていると判定した場合（Ｓ２１０６，Ｙｅｓ）、複数シナリオ併合部２４はステップＳ２１０４に戻り、複数シナリオ併合処理を継続する。
【００６６】
上記複数シナリオ併合処理の具体例について以下に説明する。  
先に述べたＤＦＤ（図２，図３、図４図５，図６参照）においては、複数シナリオが存在するのは第２の階層であるレベル２のＤＦＤに準じたシナリオ1とシナリオ2である。複数シナリオ併合部２４は、時間制約反映部２３により生成されたサブプロセスに対応する検証用追加モデル以外の検証用追加モデル、すなわち図３２に示した検証用追加モデルと、図２８に示した検証用追加モデルに基づいて、上記複数シナリオ併合処理を実行し、実行の結果として図３４に示す検証用追加モデルを生成する。複数シナリオ併合部２４は、複数シナリオ併合処理で処理しない検証用追加モデルは、そのまま出力するものとする。結果として前述した例においては、複数シナリオ併合部２４は、図31、図34、図33、図27、図29、図30のそれぞれに示した検証用追加モデルを出力することとなる。これら検証用追加モデルは、追加分検証用モデル３２としてモデル検査器４０の入力データとして使用される。
【００６７】
［２．４．検証モデル修正部の動作例；検証モデル修正処理］
次に、検証モデル修正部２１の動作例について説明する。検証モデル修正部２１は検証モデル修正処理を実行する。図２２に検証モデル修正処理の一例のフローチャートを掲げる。以下、図２２を参照しながら検証モデル修正処理を説明する。
【００６８】
検証モデル修正処理において、検証モデル修正部２１は、まず入力されたプロセスの全遷移に対して以下の処理を行う（Ｓ２２０１）。すなわち、当該遷移がいずれかのデータ送受信シーケンスのシナリオに出現するデータの送信を含むか否かを判定する（Ｓ２２０２）。データの送信を含むと判定した場合（Ｓ２２０２，Ｙｅｓ）、後述するＳ２２０４の判定処理に進む。一方、データの送信を含んでいないと判定した場合（Ｓ２２０２，Ｎｏ）、検証モデル修正部２１は、その遷移のguardに次の条件を論理和で追加する。
［条件］  上記データの送信発生を示すフラグ値＝＝送信済み
【００６９】
上記Ｓ２２０３実行後、ステップＳ２２０４に進む。ステップＳ２２０４において、検証モデル修正部２１は、上記Ｓ２２０２，Ｓ２２０３の処理を全遷移に実行したか否かを判定する（Ｓ２２０４）。すべての遷移について実行していないと判定した場合（Ｓ２２０４，Ｎｏ）、検証モデル修正部２１は、ステップＳ２００２に戻り処理を続行する。一方、すべての遷移について実行したと判定した場合（Ｓ２２０４，Ｎｏ）、検証モデル修正部２１は、検証モデル修正処理を終了する。
【００７０】
上記検証モデル修正処理の具体例について以下に説明する。  
検証モデル修正部２１に、以下の各プロセスの検証モデル、すなわちＰ１の検証モデル(図１２参照)、Ｐ２の検証モデル(図１３参照)、Ｐ３の検証モデル(図１４参照)、Ｐ４の検証モデル(図１５参照)、ＰＢの検証モデル(図１６参照)、envの検証モデル(図１７参照)が入力されたものとする。検証用モデル修正部２１は、図２２に示した検証用モデル修正処理をこれら検証用モデルに対して実行する。その結果、検証用モデル修正部２１は、それぞれＰ１の修正された検証モデル（図３５参照）、Ｐ２の修正された検証モデル（図３６参照）、Ｐ３の修正された検証モデル（図３７参照）、Ｐ４の修正された検証モデル（図３８参照）、ＰＢの修正された検証モデル（図３９参照）、envの修正された検証モデル（図４０参照）を出力する。これら修正された検証モデルは修正済み検証モデル３１としてモデル検査器４０の入力データとなる。
【００７１】
［２．５．検証式作成部の動作例；検証式作成処理］
次に、検証式生成部２５の動作例について説明する。検証式生成部２５は検証式生成処理を実行する。図２２に検証式生成処理の一例のフローチャートを掲げる。以下、図２２を参照しながら検証モデル修正処理を説明する。
【００７２】
まず、検証式生成部２５は、以下の検証式１を生成する（Ｓ２３０１）。
【００７３】
（検証式１）  A[]flag==0
次に、検証式生成部２３は以下の検証式２を生成する(Ｓ２３０２)
（検証式２）  A[]not deadlock or (α)
但し、α=すべてのシナリオに対応する"プロセス名.fin"の論理和
検証式生成部２５は上記検証式１及び検証式２を、検証式２５として出力する。出力された検証式２５はモデル検査器４０の入力として使用される。
【００７４】
上記検証式生成処理の具体例について説明する。前述した例において、最上位レベルのＤＦＤ（図２参照）に準じたシナリオに対応する検証用モデル（図３１参照）と、レベル2のＤＦＤに準じたシナリオ１とシナリオ２に対応する検証用モデル（図３４参照）にそれぞれ”flow1”、”flow2”というプロセス名が付与されたとする。この場合、検証式作成部２５は、図２３に示した検証式作成処理を実行し、その結果、図41に示す検証式を生成し、出力する。
【００７５】
［３．モデル検査器による検査結果］
本モデル検査支援装置１から出力された追加分検証用モデル３２（図31、図34、図33、図27、図29、図30参照）、及び、修正検証用モデル３１（図35、図36、図37、図38、図39、図40参照）、及び、検証式３３（図４１参照）を、モデル検査器４０の一例であるモデル検査ツールUPPAAL（URL:http://www.uppaal.com  参照）に入力した場合、モデル検査器４０が出力する検証結果画面の例を図４２に示す。図４２に示した検査結果画面では、検証式３３に含まれるそれぞれの検証式１，検証式２（図４１参照）についてメッセージ”Property is satisfied"が返されており、検証用性質の違反がないことを示している。
【００７６】
以上示したように、本実施の形態により、1以上の階層のＤＦＤと各ＤＦＤに準じたそれぞれ1以上のシナリオのデータ送受信シーケンス１２と時間制約１３、及び、いずれかの階層のコンポーネントの内部処理フローを表現した検証用モデル１１から、モデル検査の検証用性質を表現する検証用モデル（修正済み検証用モデル３１及び追加分検証用モデル３２）及び検証式３３を生成することにより、設計情報であるＤＦＤに準じたそれぞれ1以上のシナリオのデータ送受信シーケンス１２と時間制約１３を容易に有効活用して、新たな検証用性質である検証式３３を付加できる。結果として、モデル検査の検証精度が容易に向上することが期待できる。
【００７７】
［４．利点］
本モデル検査支援装置の利点は以下の通りである。
本装置によれば、1以上の階層のＤＦＤと各ＤＦＤに準じたそれぞれ1以上のシナリオのデータ送受信シーケンス、及び、いずれかの階層のコンポーネントの内部処理フローを表現した検証用モデルから、モデル検査の検証用性質を表現する検証用モデル及び検証式を生成することにより、設計情報であるＤＦＤに準じたそれぞれ1以上のシナリオのデータ送受信シーケンスと時間制約を容易に有効活用して、新たな検証用性質を付加できる。結果として、モデル検査の検証精度が容易に向上することが期待できる。
【００７８】
本装置によれば、請求項３に記載の発明によれば、入力として、複数の階層に属するコンポーネントの検証用モデルが混在するとが可能となり、それぞれ、自身及び自身よりも上位の階層に属するＤＦＤ及びそれらに準じるデータ送受信シーケンスに違反しないかを検証用性質として付加できる。
【００７９】
さらに、請求項４に記載の装置によれば、いずれかのシナリオのデータ送受信シーケンスが並行動作を含んでいた場合にも対応可能である。
【００８０】
さらに、請求項５にきさいの装置によれば、いずれかのシナリオのデータ送受信シーケンスが時間制約を含んでいた場合にも対応可能である。
【００８１】
さらに、請求項６に記載の装置によれば、いずれかの階層のＤＦＤに準じたシナリオが複数存在する場合にも対応可能である。
【図面の簡単な説明】
【００８２】
【図１】モデル検査支援装置の構成を示す機能ブロック図
【図２】最上位階層のＤＦＤとシナリオ、時間制約の例を示す図
【図３】レベル２のＤＦＤとシナリオ１、時間制約の例を示す図
【図４】レベル２のＤＦＤとシナリオ２、時間制約の例を示す図
【図５】図３のシナリオ1のデータ送受信シーケンス例を示す図
【図６】図３のシナリオ2のデータ送受信シーケンス例を示す図
【図７】最上位階層のＤＦＤのシナリオのデータ送受信シーケンスのデータ構成例を示す図
【図８】最上位階層のＤＦＤの時間制約のデータ構成例を示す図
【図９】レベル２のＤＦＤのシナリオ１のデータ送受信シーケンスのデータ構成例を示す図
【図１０】レベル２のＤＦＤのシナリオ１の時間制約のデータ構成例を示す図
【図１１】レベル２のＤＦＤのシナリオ２のデータ送受信シーケンスのデータ構成例を示す図
【図１２】コンポーネントＰ１のプロセスの内部フローを表現する検証用モデルを示す図
【図１３】コンポーネントＰ２のプロセスの内部フローを表現する検証用モデルを示す図
【図１４】コンポーネントＰ３のプロセスの内部フローを表現する検証用モデルを示す図
【図１５】コンポーネントＰ４のプロセスの内部フローを表現する検証用モデルを示す図
【図１６】コンポーネントＰＢのプロセスの内部フローを表現する検証用モデルを示す図
【図１７】環境envのプロセスの内部フローを表現する検証用モデルを示す図
【図１８】検証用追加モデル生成部による検証用追加モデル生成処理の例を示すフローチャート
【図１９Ａ】並行して動作する処理を含む場合の検証用追加モデル生成部による検証用追加モデル生成処理の例を示すフローチャート
【図１９Ｂ】図１９Ａの分岐Ａ，Ｂに繋がるフローチャート
【図２０】時間制約反映部による時間制約反映処理の例を示すフローチャート
【図２１】複数シナリオ併合部による複数シナリオ併合処理の例を示すフローチャート
【図２２】検証モデル修正部による検証モデル修正処理の例を示すフローチャート
【図２３】検証式作成部による検証式生成処理の例を示すフローチャート
【図２４】図７の検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図２５】図９の検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図２６】図９の検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図２７】図９の検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図２８】図１１の検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図２９】図１１検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図３０】図１１検証用追加モデルを入力とする検証用追加モデル生成部の出力例を示す図
【図３１】図８の時間制約と図２４の検証用追加モデルを入力とする時間制約反映部の出力例を示す図
【図３２】図１０の時間制約と図２５の検証用追加モデルを入力とする時間制約反映部の出力例を示す図
【図３３】図１０の時間制約と図２６の検証用追加モデルを入力とする時間制約反映部の出力例を示す図
【図３４】複数シナリオ併合部の出力例を示す図
【図３５】検証用モデル修正部によるＰ１のプロセスの検証用モデルの修正例を示す図
【図３６】検証用モデル修正部によるＰ２のプロセスの検証用モデルの修正例を示す図
【図３７】検証用モデル修正部によるＰ３のプロセスの検証用モデルの修正例を示す図
【図３８】検証用モデル修正部によるＰ４のプロセスの検証用モデルの修正例を示す図
【図３９】検証用モデル修正部によるＰＢのプロセスの検証用モデルの修正例を示す図
【図４０】検証用モデル修正部によるenvのプロセスの検証用モデルの修正例を示す図
【図４１】検証式作成部の出力例を示す図
【図４２】モデル検査器の出力例を示す図
【符号の説明】
【００８３】
１    …  モデル検査支援装置
２１  …  検証モデル修正部
２２  …  追加モデル生成部
２３  …  時間制約反映部
２４  …  複数シナリオ併合部
２５  …  検証式作成部
【図１】
2010026704.tif 000003
【図２】
2010026704.tif 000004
【図３】
2010026704.tif 000005
【図４】
2010026704.tif 000006
【図５】
2010026704.tif 000007
【図６】
2010026704.tif 000008
【図７】
2010026704.tif 000009
【図８】
2010026704.tif 000010
【図９】
2010026704.tif 000011
【図１０】
2010026704.tif 000012
【図１１】
2010026704.tif 000013
【図１２】
2010026704.tif 000014
【図１３】
2010026704.tif 000015
【図１４】
2010026704.tif 000016
【図１５】
2010026704.tif 000017
【図１６】
2010026704.tif 000018
【図１７】
2010026704.tif 000019
【図１８】
2010026704.tif 000020
【図１９Ａ】
2010026704.tif 000021
【図１９Ｂ】
2010026704.tif 000022
【図２０】
2010026704.tif 000023
【図２１】
2010026704.tif 000024
【図２２】
2010026704.tif 000025
【図２３】
2010026704.tif 000026
【図２４】
2010026704.tif 000027
【図２５】
2010026704.tif 000028
【図２６】
2010026704.tif 000029
【図２７】
2010026704.tif 000030
【図２８】
2010026704.tif 000031
【図２９】
2010026704.tif 000032
【図３０】
2010026704.tif 000033
【図３１】
2010026704.tif 000034
【図３２】
2010026704.tif 000035
【図３３】
2010026704.tif 000036
【図３４】
2010026704.tif 000037
【図３５】
2010026704.tif 000038
【図３６】
2010026704.tif 000039
【図３７】
2010026704.tif 000040
【図３８】
2010026704.tif 000041
【図３９】
2010026704.tif 000042
【図４０】
2010026704.tif 000043
【図４１】
2010026704.tif 000044
【図４２】
2010026704.tif 000045