(57)【要約】【課題】モデル検査に精通していない設計者が容易にモデル検査ツールを使いこなすことができるモデル検査用情報生成装置を提供する。【解決手段】各リアルタイムプロセスの状態遷移図３１の各遷移に対して遷移元ロケーションにおけるアクション名と遷移先ロケーションにおけるアクション名から構成される名称の放送型通信チャネルを追加定義するとともに、放送型通信チャネルへの送信イベントを当該遷移における処理として追加して修正版状態遷移図４１を生成する遷移抽出イベント挿入手段２１と、ロケーションとシーケンスチャート３２上の連続した２つのアクション名から構成される放送型通信チャネルの受信を処理する２つのアクション名に対応する各ロケーション間の遷移とから構成されるオブザーバ４２を生成するオブザーバ生成手段２２と、オブザーバ４２のプロセスに基づいて検証したい性質を記述する検証式４３を生成する検証式生成手段２３とを備える。【選択図】        図２
2008021160.tif 000002
【特許請求の範囲】
【請求項１】
時間情報を含むリアルタイムプロセスの状態遷移図と当該状態遷移図で表現される前記リアルタイムプロセスの挙動の一部分であり時間要求を含むシーケンスチャートとに基づき、前記リアルタイムプロセスのモデル検査に必要な修正版状態遷移図とオブザーバと検証式とを生成するモデル検査用情報生成装置であって、
前記リアルタイムプロセスの前記状態遷移図および前記シーケンスチャートに基づき、前記リアルタイムプロセスの前記状態遷移図の各遷移に対して遷移元ロケーションにおけるアクション名と遷移先ロケーションにおけるアクション名から構成される名称の１対多の通信である放送型通信チャネルを追加定義するとともに、前記放送型通信チャネルへの送信イベントを当該遷移における処理として前記状態遷移図に追加して前記修正版状態遷移図を生成して、前記リアルタイムプロセスの状態遷移履歴を通知可能とする遷移抽出イベント挿入手段と、
前記状態遷移図と前記シーケンスチャートとに基づき、前記シーケンスチャート上の各アクションに対応した名称であるロケーションと前記シーケンスチャート上の連続した２つのアクション名から構成される前記放送型通信チャネルの受信を処理する前記２つのアクション名に対応する前記各ロケーション間の遷移とから構成され、前記放送型通信チャネルを介して通知される前記リアルタイムプロセスの状態遷移履歴に対応して状態が遷移する前記オブザーバを生成するオブザーバ生成手段と、
このオブザーバ生成手段により生成された前記オブザーバのプロセスに基づいて検証したい性質を記述する前記検証式を生成する検証式生成手段と、
を備えることを特徴とするモデル検査用情報生成装置。
【請求項２】
前記遷移抽出イベント挿入手段は、前記リアルタイムプロセスの前記状態遷移図の各遷移に対して、遷移元ロケーションにおけるアクション名から構成される名称の放送型通信チャネルを追加定義するとともに、前記放送型通信チャネルへの送信イベントを当該遷移における処理として追加する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項３】
前記オブザーバ生成手段により生成される前記オブザーバは、不整合が生じた際にエラー状態に遷移する状態遷移を有する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項４】
前記オブザーバ生成手段は、前記シーケンスチャートに含まれる時間に関する要求仕様を有する各アクションに対して、通知される状態遷移履歴が要求仕様を満たす場合に、前記シーケンスチャート上の次の状態に遷移可能な遷移を生成するとともに、通知される状態遷移履歴が要求仕様を満たさない場合にエラー状態に遷移する遷移を生成する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項５】
前記オブザーバ生成手段は、前記シーケンスチャートに含まれる時間に関する宣言を有する各アクションに対して、通知される状態遷移履歴が宣言に合致する場合のみ前記シーケンスチャート上の次の状態に遷移可能な遷移を生成する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項６】
前記オブザーバ生成手段は、前記シーケンスチャート上のアクションに対して、アクション名から構成されるロケーションと初期ロケーションの間に当該アクション名から構成されるチャネルを受信する遷移を生成することによって状態遷移履歴がシーケンスから外れた場合に前記オブザーバは初期ロケーションに遷移する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項７】
前記検証式生成手段は、生成された前記オブザーバのエラー状態のロケーションに、いかなる実行パスのいかなる時刻においても、到達しないことを示す検証式を生成する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項８】
前記検証式生成手段は、生成された前記オブザーバの最後のロケーションに到達する実行パスが存在することを示す検証式を生成する、
ことを特徴とする請求項１記載のモデル検査用情報生成装置。
【請求項９】
前記シーケンスチャートに同一のロケーションが複数回含まれ、前記オブザーバが該ロケーションを現在の状態と認識している場合に、当該ロケーションを遷移元とする状態遷移履歴が通知された際に、前記シーケンスチャート中のより前方に存在する同一名のロケーションも現在状態として認識可能とすることを特徴とするオブザーバ再入可能化手段を備える、
ことを特徴とする請求項６記載のモデル検査用情報生成装置。
【請求項１０】
時間情報を含むリアルタイムプロセスの状態遷移図と当該状態遷移図で表現される前記リアルタイムプロセスの一部分であり時間要求を含むシーケンスチャートとに基づき、前記リアルタイムプロセスのモデル検査に必要な修正版状態遷移図とオブザーバと検証式とを生成する処理をコンピュータに実行させるプログラムであって、
前記リアルタイムプロセスの前記状態遷移図および前記シーケンスチャートに基づき、リアルタイムプロセスの前記状態遷移図の各遷移に対して遷移元ロケーションにおけるアクション名と遷移先ロケーションにおけるアクション名から構成される名称の１対多の通信である放送型通信チャネルを追加定義するとともに、該遷チャネルへの送信イベントを該遷移における処理として前記状態遷移図に追加して前記修正版状態遷移図を生成して、前記各リアルタイムプロセスの状態遷移履歴を通知可能とする遷移抽出イベント挿入機能と、
前記状態遷移図と前記シーケンスチャートとに基づき、前記シーケンスチャート上の各アクションに対応した名称であるロケーションと前記シーケンスチャート上の連続した２つのアクション名から構成される前記放送型通信チャネルの受信を処理する前記２つのアクション名に対応する前記各ロケーション間の遷移とから構成され、前記放送型通信チャネルを介して通知される前記各リアルタイムプロセスの状態遷移履歴に対応して状態が遷移する前記オブザーバを生成するオブザーバ生成機能と、
このオブザーバ生成機能により生成された前記オブザーバのプロセスに基づいて検証したい性質を記述する前記検証式を生成する検証式生成機能と、
を前記コンピュータに実行させることを特徴とするプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、リアルタイムプロセスの設計情報での挙動検証技術に係わるリアルタイムプロセスのモデル検査用監視オートマトン生成装置などのモデル検査用情報生成装置およびプログラムに関する。
【背景技術】
【０００２】
イベントが発生する時間に基づいて挙動が決定される、あるいは、システムの動作時間に関して制約や要求仕様があるようなリアルタイムシステム分野および組込みシステム分野においては、その挙動の検証が重要かつ難解である。この様な分野の典型的なシステムとしては、ネットワークを介した通信プロトコルシステム、複数のロボットによる協調動作システムなどがある。
【０００３】
そこで、上述したような分野では、挙動検証のためにモデル検査技術が使われることが多い。時間制約や性能に関して検証可能な代表的なモデル検査ツールとしては、スウェーデンのUppsala大学とデンマークのAlborg大学が共同で開発した“UPPAAL”などがある。“UPPAAL”は、時間オートマトンに論理型変数や整数型変数といった一般的なデータを付加した拡張時間オートマトンの並列動作モデルを記述でき、その振る舞いの不変性および可到達性の検証をモデルチェック機能により行うことができるツールである。“UPPAAL”は、システムの状態遷移モデルをＧＵＩで描くことができるので、モデルの記述が簡単であるという特徴を有している。
【０００４】
ところで、リアルタイムシステム分野および組込システム分野における一般的なシステム設計プロセスでは、状態遷移表、状態遷移図（ステートチャート）、シーケンスチャート、タイミングチャートなどが作成されるが、モデル検査を実施するためには、状態遷移図に漏れなく時間情報を追加するとともに、検証したい性質を記述する検証式を作製する必要がある。このうち、状態遷移図に詳細な時間情報を追加する作業は、設計の詳細化プロセスに必須の作業であって従来から設計者によって実施されている作業であるが、検証式の作成はモデル検査技術特有の作業であり、ほとんどの設計者にとっては不可能に近い作業である。
【０００５】
これに対して、非特許文献１では、シーケンスチャートからobserverと呼ばれる状態遷移図で定義されたシステム挙動を監視する状態遷移を生成し、このobserverと簡単な検証式の組み合わせで挙動の検証を実現する手法が提案されている。
【０００６】
【非特許文献１】“Timed Sequence Diagrams and Tool-Based Analysis A Case Study”, Thomas Firley, Michaela Huhn, Karsten Diethers, Thomas Gehrke, and Ursula Goltz,
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、非特許文献１で提案されているような手法においては、現実の設計プロセスに対応していない課題がいくつかある。
【０００８】
第１に、シーケンスチャートには、要求仕様としての時間制約が記載される場合の他に、挙動の一例としての時間宣言が記載される場合もあるが、非特許文献１で提案されているような手法では、要求仕様としての時間制約のみにしか対応していないという問題がある。
【０００９】
第２に、設計段階で作成されるシーケンスチャートは、状態遷移図で表現されるシステム挙動の一部分であり、かつ、そのようなシーケンスチャートが多数作成されるが、非特許文献１で提案されているような手法では、複数のシーケンスチャートを効果的に扱えないという問題がある。
【００１０】
第３に、モデル検査ではリアルタイムプロセス毎に挙動を状態遷移図で定義するために複数の状態遷移図から構成され、シーケンスチャートにも複数の構成要素の挙動が記載されるが、非特許文献１で提案されているような手法では、単一のシステム要素に対する単一の状態遷移図を対象としているという問題がある。
【００１１】
本発明は、上記に鑑みてなされたものであって、モデル検査に精通していない設計者が容易にモデル検査ツールを使いこなすことができるモデル検査用情報生成装置およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【００１２】
上述した課題を解決し、目的を達成するために、本発明は、時間情報を含むリアルタイムプロセスの状態遷移図と当該状態遷移図で表現される前記リアルタイムプロセスの挙動の一部分であり時間要求を含むシーケンスチャートとに基づき、前記リアルタイムプロセスのモデル検査に必要な修正版状態遷移図とオブザーバと検証式とを生成するモデル検査用情報生成装置であって、前記リアルタイムプロセスの前記状態遷移図および前記シーケンスチャートに基づき、前記リアルタイムプロセスの前記状態遷移図の各遷移に対して遷移元ロケーションにおけるアクション名と遷移先ロケーションにおけるアクション名から構成される名称の１対多の通信である放送型通信チャネルを追加定義するとともに、前記放送型通信チャネルへの送信イベントを当該遷移における処理として前記状態遷移図に追加して前記修正版状態遷移図を生成して、前記リアルタイムプロセスの状態遷移履歴を通知可能とする遷移抽出イベント挿入手段と、前記状態遷移図と前記シーケンスチャートとに基づき、前記シーケンスチャート上の各アクションに対応した名称であるロケーションと前記シーケンスチャート上の連続した２つのアクション名から構成される前記放送型通信チャネルの受信を処理する前記２つのアクション名に対応する前記各ロケーション間の遷移とから構成され、前記放送型通信チャネルを介して通知される前記リアルタイムプロセスの状態遷移履歴に対応して状態が遷移する前記オブザーバを生成するオブザーバ生成手段と、このオブザーバ生成手段により生成された前記オブザーバのプロセスに基づいて検証したい性質を記述する前記検証式を生成する検証式生成手段と、を備える。
【００１３】
また、本発明は、時間情報を含むリアルタイムプロセスの状態遷移図と当該状態遷移図で表現される前記リアルタイムプロセスの一部分であり時間要求を含むシーケンスチャートとに基づき、前記リアルタイムプロセスのモデル検査に必要な修正版状態遷移図とオブザーバと検証式とを生成する処理をコンピュータに実行させるプログラムであって、前記リアルタイムプロセスの前記状態遷移図および前記シーケンスチャートに基づき、リアルタイムプロセスの前記状態遷移図の各遷移に対して遷移元ロケーションにおけるアクション名と遷移先ロケーションにおけるアクション名から構成される名称の１対多の通信である放送型通信チャネルを追加定義するとともに、該遷チャネルへの送信イベントを該遷移における処理として前記状態遷移図に追加して前記修正版状態遷移図を生成して、前記各リアルタイムプロセスの状態遷移履歴を通知可能とする遷移抽出イベント挿入機能と、前記状態遷移図と前記シーケンスチャートとに基づき、前記シーケンスチャート上の各アクションに対応した名称であるロケーションと前記シーケンスチャート上の連続した２つのアクション名から構成される前記放送型通信チャネルの受信を処理する前記２つのアクション名に対応する前記各ロケーション間の遷移とから構成され、前記放送型通信チャネルを介して通知される前記各リアルタイムプロセスの状態遷移履歴に対応して状態が遷移する前記オブザーバを生成するオブザーバ生成機能と、このオブザーバ生成機能により生成された前記オブザーバのプロセスに基づいて検証したい性質を記述する前記検証式を生成する検証式生成機能と、を前記コンピュータに実行させる。
【発明の効果】
【００１４】
本発明によれば、モデル検査に必要な検証式を設計者が作成することなく、かつ、１対多の通信である放送型通信チャネルを利用することで元のソフトウェアモデルには影響を与えずに、現実の設計プロセスにおいて作成される複数のシーケンスチャートに記述された要件（時間に対する要求仕様、時間宣言）が用意された状態遷移の設計で満たされるかどうかを検証するモデル検査のために必要な情報が自動生成されるので、モデル検査に精通していない設計者が容易にモデル検査ツールを使いこなすことができる、という効果を奏する。
【発明を実施するための最良の形態】
【００１５】
以下に添付図面を参照して、この発明にかかるモデル検査用情報生成装置およびプログラムの最良な実施の形態を詳細に説明する。
【００１６】
［第１の実施の形態］
本発明の第１の実施の形態を図１ないし図１５に基づいて説明する。図１は、本発明の第１の実施の形態にかかるモデル検査用監視オートマトン生成装置１のハードウェア構成を示すブロック図である。本実施の形態のモデル検査用監視オートマトン生成装置１は、モデル検査用情報生成装置であって、概略的には、設計プロセスにおいて作成される複数のシーケンスチャートに記述された要件（時間に対する要求仕様、時間宣言）が用意された状態遷移の設計で満たされるかどうかを検証するモデル検査のために必要な入力情報を自動生成するものである。
【００１７】
図１に示すように、モデル検査用監視オートマトン生成装置１は、例えばパーソナルコンピュータやワークステーションであり、コンピュータの主要部であって各部を集中的に制御するＣＰＵ（Central Processing Unit）２を備えている。このＣＰＵ２には、ＢＩＯＳなどを記憶した読出し専用メモリであるＲＯＭ（Read Only Memory）３と、各種データを書換え可能に記憶するＲＡＭ（Random Access Memory）４とがバス５で接続されている。
【００１８】
さらにバス５には、各種のプログラム等を格納するＨＤＤ（Hard Disk Drive）６と、配布されたプログラムであるコンピュータソフトウェアを読み取るための機構としてＣＤ（Compact Disc）−ＲＯＭ７を読み取るＣＤ−ＲＯＭドライブ８と、モデル検査用監視オートマトン生成装置１とネットワーク９との通信を司る通信制御装置１０と、各種操作指示を行うキーボードやマウスなどの入力装置１１と、各種情報を表示するＣＲＴ（Cathode Ray Tube）、ＬＣＤ（Liquid Crystal Display）などの表示装置１２とが、図示しないＩ／Ｏを介して接続されている。
【００１９】
ＲＡＭ４は、各種データを書換え可能に記憶する性質を有していることから、ＣＰＵ２の作業エリアとして機能してバッファ等の役割を果たす。
【００２０】
図１に示すＣＤ−ＲＯＭ７は、この発明の記憶媒体を実施するものであり、ＯＳ（Operating System）や各種のプログラムが記憶されている。ＣＰＵ２は、ＣＤ−ＲＯＭ７に記憶されているプログラムをＣＤ−ＲＯＭドライブ８で読み取り、ＨＤＤ６にインストールする。
【００２１】
なお、記憶媒体としては、ＣＤ−ＲＯＭ７のみならず、ＤＶＤなどの各種の光ディスク、各種光磁気ディスク、フレキシブル・ディスクなどの各種磁気ディスク等、半導体メモリ等の各種方式のメディアを用いることができる。また、通信制御装置１０を介してインターネットなどのネットワーク９からプログラムをダウンロードし、ＨＤＤ６にインストールするようにしてもよい。この場合に、送信側のサーバでプログラムを記憶している記憶装置も、この発明の記憶媒体である。なお、プログラムは、所定のＯＳ（Operating System）上で動作するものであってもよいし、その場合に後述の各種処理の一部の実行をＯＳに肩代わりさせるものであってもよいし、所定のアプリケーションソフトやＯＳなどを構成する一群のプログラムファイルの一部として含まれているものであってもよい。
【００２２】
このシステム全体の動作を制御するＣＰＵ２は、このシステムの主記憶として使用されるＨＤＤ６上にロードされたプログラムに基づいて各種処理を実行する。
【００２３】
次に、モデル検査用監視オートマトン生成装置１のＨＤＤ６にインストールされている各種のプログラムがＣＰＵ２に実行させる機能のうち、本実施の形態のモデル検査用監視オートマトン生成装置１が備える特長的な機能について説明する。
【００２４】
図２は、モデル検査用監視オートマトン生成装置１の機能構成を示すブロック図である。図２に示すように、モデル検査用監視オートマトン生成装置１は、モデル検査用監視オートマトン生成プログラムに従うことにより、遷移抽出イベント挿入手段である遷移抽出イベント挿入部２１と、オブザーバ（observer（状態遷移図で定義されたシステム挙動を監視する状態遷移図））４２を生成するオブザーバ生成手段であるobserver生成部２２と、検証式４３を生成する検証式生成手段である検証式生成部２３とを備える。
【００２５】
遷移抽出イベント挿入部２１は、時間情報を含む複数のプロセスの状態遷移図３１と、時間要求を含む複数のシーケンスチャート３２とから、各プロセスの状態遷移履歴を他のプロセスに通知する状態および遷移を抽出して状態遷移図３１に追加して修正版状態遷移図４１を生成する。ここで、状態遷移図３１は、時間制約や性能に関して検証可能なモデル検査ツール“UPPAAL”に用いられる状態遷移図である。“UPPAAL”は、時間オートマトンに論理型変数や整数型変数といった一般的なデータを付加した拡張時間オートマトンの並列動作モデルを記述でき、その振る舞いの不変性および可到達性の検証をモデルチェック機能により行うことができるツールである。“UPPAAL”は、システムの状態遷移モデルをＧＵＩで描くことができるので、モデルの記述が簡単であるという特徴を有している。また、シーケンスチャート３２は、リアルタイムシステム設計に用いられるＵＭＬ profile for ＳＰＴ（リアルタイムシステムの設計言語の規格）によるシーケンスチャートである。
【００２６】
observer生成部２２は、状態遷移図３１と個々のシーケンスチャート３２とに基づき、状態遷移履歴の通知と不整合が生じた際にエラー状態に遷移する状態遷移を有するプロセスのobserver４２を新たに生成する。
【００２７】
検証式生成部２３は、個々のシーケンスチャート３２に基づいて生成された個々のobserverプロセスがいかなる場合でもエラー状態に遷移されないことを検証する検証式４３、およびobserverプロセスの最後のロケーションに到達する場合が存在することを検証する検証式４３を生成する。
【００２８】
まず、遷移抽出イベント挿入部２１について詳述する。ここで、図３は遷移抽出イベント挿入部２１における遷移抽出イベント挿入処理の流れを示すフローチャートである。図３に示すように、全ての状態遷移図３１の全ロケーションに対して終了しておらず（ステップＳ１のＮｏ）、注目しているロケーションがいずれかのシーケンスチャートに出現している場合には（ステップＳ２のＹｅｓ）、注目しているロケーションを名前に持つ放送型通信チャンネル宣言を追加した後（ステップＳ３）、ステップＳ４に進み、注目しているロケーションの全ての次ロケーションに対して終了しているか否かを判断する。
【００２９】
注目しているロケーションの全ての次ロケーションに対して終了していない場合には（ステップＳ４のＮｏ）、注目している次ロケーションの直前に、時間経過０のロケーションと、注目しているロケーションを名前に持つ１対多の通信である放送型通信チャネルへの送信を行う遷移を挿入する（ステップＳ５）。
【００３０】
そして、注目している次ロケーションがいずれかのシーケンスチャートに出現している場合には（ステップＳ６のＹｅｓ）、注目しているロケーションと注目している次ロケーションの組を名前に持つ放送型通信チャンネル宣言を追加し（ステップＳ７）、注目している次ロケーションの直前に、時間経過０のロケーションと、上記放送型通信チャネルへの送信を行う遷移を挿入して（ステップＳ８）、ステップＳ４に戻る。
【００３１】
なお、注目している次ロケーションがいずれかのシーケンスチャートに出現していない場合には（ステップＳ６のＮｏ）、そのままステップＳ４に戻る。
【００３２】
上述したようなステップＳ４〜ステップＳ８の処理は、注目しているロケーションの全ての次ロケーションに対して終了していると判断されるまで（ステップＳ４のＹｅｓ）、繰り返される。注目しているロケーションの全ての次ロケーションに対して終了している場合には（ステップＳ４のＹｅｓ）、ステップＳ９に進み、注目しているロケーションの全ての前ロケーションに対して終了しているか否かを判断する。
【００３３】
注目しているロケーションの全ての前ロケーションに対して終了していない場合には（ステップＳ９のＮｏ）、注目している次ロケーションの直前に、時間経過０のロケーションと、注目しているロケーションを名前に持つ放送型通信チャネルへの送信を行う遷移を挿入する（ステップＳ１０）。
【００３４】
そして、注目している前ロケーションがいずれかのシーケンスチャートに出現していない場合には（ステップＳ１１のＮｏ）、注目している前ロケーションと注目しているロケーションの組を名前に持つ放送型通信チャンネル宣言を追加し（ステップＳ１２）、注目している前ロケーションからの遷移に、注目しているロケーションの直前に時間経過０のロケーションと、上記放送型通信チャネルへの送信を行う遷移を挿入して（ステップＳ１３）、ステップＳ９に戻る。
【００３５】
なお、注目している前ロケーションがいずれかのシーケンスチャートに出現している場合には（ステップＳ１１のＹｅｓ）、そのままステップＳ９に戻る。
【００３６】
上述したようなステップＳ９〜ステップＳ１３の処理は、注目しているロケーションの全ての前ロケーションに対して終了していると判断されるまで（ステップＳ９のＹｅｓ）、繰り返される。注目しているロケーションの全ての前ロケーションに対して終了している場合には（ステップＳ９のＹｅｓ）、ステップＳ１に戻る。
【００３７】
以上説明したようなステップＳ１〜ステップＳ１３の処理は、全ての状態遷移図３１の全ロケーションに対して終了したと判断されるまで（ステップＳ１のＹｅｓ）、繰り返される。
【００３８】
ここで、図４は遷移抽出イベントが挿入される状態を示す模式図である。ここでは、図４に示すような状態遷移図３１およびシーケンスチャート３２が入力された場合の動作例を示す。
【００３９】
遷移抽出イベント挿入部２１における遷移抽出イベント挿入処理に従うことにより、図４に示すように、ロケーションａ１に対して、ロケーションａ０とａ１を含む「Ａ．０ ｔｏ Ａ．１」という名前の放送型通信チャネルとａ０を名前に含む「Ａ．０」という名前の放送型通信チャネルの定義宣言である「broadcast chan Ａ．０ ｔｏ Ａ．１，Ａ．０；」を追加する。すなわち、各プロセスの状態遷移図３１の各遷移に対して、遷移元ロケーションにおけるアクション名と遷移先ロケーションにおけるアクション名から構成される名称の放送型通信チャネルを追加定義し、遷移元ロケーションにおけるアクション名から構成される名称の放送型通信チャネルを追加定義するとともに、該遷移に対して、該遷移チャネルへの送信イベントを追加する。これにより、どう動いているかを把握することができる。
【００４０】
さらに、図４に示すように、ロケーションａ０とａ１の間に、時間経過０のノードが“２”挿入されるとともに、チャネル「Ａ．０ ｔｏ Ａ．１」を受信する遷移とチャネル「Ａ．０」を受信するチャネルが挿入される。同様に、ロケーションａ２に対して、ロケーションａ１とａ２を含む「Ａ．１ ｔｏ Ａ．２」という名前の放送型通信チャネルとａ１を名前に含む「Ａ．１」という名前の放送型通信チャネルの定義宣言である「broadcast chan Ａ．１ ｔｏ Ａ．２，Ａ．１；」を追加する。さらに、ロケーションａ１とａ２の間に、時間経過０のノードが“２”挿入されるとともに、チャネル「Ａ．１ ｔｏ Ａ．２」を受信する遷移とチャネル「Ａ．１」を受信するチャネルが挿入される。
【００４１】
次に、observer生成部２２について詳述する。ここで、図５はobserver生成部２２におけるobserver生成処理の流れを示すフローチャート、図６はobserver生成処理の一部の処理の流れを示すフローチャートである。図５に示すように、observer生成部２２は、シーケンスチャート３２に含まれる全プロセスに対して、注目するプロセス単体のシーケンスのみを抽出して「observer」を生成する（ステップＳ２１のＮｏ，ステップＳ２２）。
【００４２】
ステップＳ２２における処理について図６に示すフローチャートを参照しつつ詳述する。図６に示すように、まず、initialロケーションとfailロケーション、シーケンスチャートの最初のロケーション定義を追加するとともに、専用のclock変数の定義を追加する（ステップＳ３１）。
【００４３】
次いでステップＳ３２に進み、シーケンスチャートの最初のロケーションに対応する状態遷移図のロケーションの全ての前ロケーションに対して終了していない場合には（ステップＳ３２のＮｏ）、initialロケーションとfailロケーションとの間に、該全ロケーションと最初の組を名前として持つチャネルの受信を行う遷移を追加する（ステップＳ３３）。
【００４４】
このようなステップＳ３２〜Ｓ３３の処理は、シーケンスチャートの最初のロケーションに対応する状態遷移図のロケーションの全ての前ロケーションに対して終了していると判断されるまで（ステップＳ３２のＹｅｓ）、繰り返される。シーケンスチャートの最初のロケーションに対応する状態遷移図のロケーションの全ての前ロケーションに対して終了していると判断された場合には（ステップＳ３２のＹｅｓ）、ステップＳ３４に進み、シーケンスチャートの全てのロケーションに対して終了しているか否かを判断する。
【００４５】
シーケンスチャートの全てのロケーションに対して終了しておらず（ステップＳ３４のＮｏ）、注目しているロケーションが時間要求仕様を持っており（ステップＳ３５のＹｅｓ）、注目しているロケーションの全ての次ロケーションに対して終了していない場合には（ステップＳ３６のＮｏ）、時間経過０のロケーションを追加して、注目ロケーションから追加したロケーションへ、要求仕様をguardとする遷移を追加するとともに（ステップＳ３７）、シーケンスチャートの次のロケーションを名前に持つロケーションを追加して、上記追加した時間経過０のロケーションから、次ロケーションへ、注目ロケーションと次ロケーションを名前に持つチャネルの受信を行い、専用のclock変数を０にする遷移を追加して（ステップＳ３８）、ステップＳ３６に戻る。
【００４６】
このようなステップＳ３６〜Ｓ３８の処理は、注目しているロケーションの全ての次ロケーションに対して終了していると判断されるまで（ステップＳ３６のＹｅｓ）、繰り返される。
【００４７】
注目しているロケーションの全ての次ロケーションに対して終了していると判断されると（ステップＳ３６のＹｅｓ）、時間経過０のロケーションを追加して、注目ロケーションから追加した時間０のロケーションへ、要求仕様のnotをguardとする遷移を追加するとともに（ステップＳ３９）、上記追加した時間経過０のロケーションから、failロケーションへ、注目ロケーションと次ロケーションを名前に持つチャネルの受信を行い、専用のclock変数０にする遷移を追加した後（ステップＳ４０）、ステップＳ４１に進み、注目しているロケーションが、時間性能宣言を持つか否かを判断する。
【００４８】
なお、前述したステップＳ３５において、注目しているロケーションが時間要求仕様を持っていないと判断した場合も（ステップＳ３５のＮｏ）、ステップＳ４１に進み、注目しているロケーションが、時間性能宣言を持つか否かを判断する。
【００４９】
注目しているロケーションが、時間性能宣言を持つと判断し（ステップＳ４１のＹｅｓ）、注目しているロケーションの全ての次ロケーションに対して終了していない場合には（ステップＳ４２のＮｏ）、時間経過０のロケーションを追加して、注目ロケーションから追加したロケーションへ、要求仕様をguardとする遷移を追加するとともに（ステップＳ４３）、シーケンスチャートの次のロケーションを名前に持つロケーションを追加して、上記追加した時間経過０のロケーションから、次ロケーションへ、注目ロケーションと次ロケーションを名前に持つチャネルの受信を行う遷移を追加して（ステップＳ４４）、ステップＳ４２に戻る。
【００５０】
このようなステップＳ４２〜Ｓ４４の処理は、注目しているロケーションの全ての次ロケーションに対して終了していると判断されるまで（ステップＳ４２のＹｅｓ）、繰り返される。
【００５１】
そして、注目しているロケーションの全ての次ロケーションに対して終了していると判断した場合（ステップＳ４２のＹｅｓ）、または、注目しているロケーションが、時間性能宣言を持たないと判断した場合には（ステップＳ４１のＮｏ）、ステップＳ４５に進み、注目しているロケーションが時間要求仕様も時間性能宣言も持たないか否かを判断する。
【００５２】
注目しているロケーションが時間要求仕様も時間性能宣言も持たないと判断した場合には（ステップＳ４５のＹｅｓ）、注目しているロケーションから次ロケーションへ、注目ロケーションと次ロケーションを名前に持つチャネルの受信を行い、専用のclock変数を０にする遷移を追加して（ステップＳ４６）、ステップＳ３４に戻る。一方、注目しているロケーションが時間要求仕様か時間性能宣言を持っていると判断した場合には（ステップＳ４５のＮｏ）、そのままステップＳ３４に戻る。
【００５３】
以上説明したようなステップＳ３４〜Ｓ４６の処理は、シーケンスチャートの全てのロケーションに対して終了していると判断されるまで（ステップＳ３４のＹｅｓ）、繰り返される。
【００５４】
シーケンスチャートの全てのロケーションに対して終了していると判断された場合には（ステップＳ３４のＹｅｓ）、注目しているロケーションからinitロケーションへ、注目しているロケーションを名前に持つチャネルの受信を行う遷移を追加して（ステップＳ４７）、ステップＳ２２における処理を終了する。
【００５５】
続いて、検証式生成部２３について詳述する。ここで、図７は検証式生成部２３における検証式生成処理の流れを示すフローチャートである。図７に示すように、検証式生成部２３は、全てのシーケンスチャートの全ロケーションに対して終了しておらず（ステップＳ５１のＮｏ）、注目シーケンスチャートが要求仕様を含む場合には（ステップＳ５２のＹｅｓ）、検証式“Ａ［］（not 該シーケンスチャートに対応するobserver名．Fail）”を追加するとともに（ステップＳ５３）、検証式“Ｅ＜＞（該シーケンスチャートに対応するobserver名．最後のロケーション名）”を追加して（ステップＳ５４）、ステップＳ５１に戻る。一方、注目シーケンスチャートが要求仕様を含まない場合には（ステップＳ５２のＮｏ）、検証式“Ｅ＜＞（該シーケンスチャートに対応するobserver名．最後のロケーション名）”のみを追加して（ステップＳ５４）、ステップＳ５１に戻る。
【００５６】
以上説明したようなステップＳ５１〜Ｓ５４の処理は、全てのシーケンスチャートの全ロケーションに対して終了するまで（ステップＳ５１のＹｅｓ）、繰り返される。
【００５７】
ここで、図８はobserver生成（要求仕様のケース）および検証式生成を示す模式図である。ここでは、図８に示すようなシーケンスチャート３２が入力された場合の動作例を示す。
【００５８】
入力されたシーケンスチャート３２は、「Process Ａ」という名前のプロセスにおいて、「ReqZeroToruque」という名前のチャネルを受信後、ロケーション「１」のアクションが実施され、４００［ｍｓ］以内に該アクションが終了して、「ZeroToruque」という名前のチャネルに送信後、次ロケーションに遷移することを表現している。ここで、“SAworstCase”という用語は、リアルタイムシステムの設計言語の規格であるＵＭＬ profile for ＳＰＴで用いられている用語であり、該アクションの最大実行時間に対する要求仕様を意味するものである。このようなシーケンスチャート３２を入力すると、observer生成部２２は、図５および図６に示したobserver生成処理に従うことにより、図８に示すようなobserver４２を生成する。
【００５９】
すなわち、observer生成部２２は、図８に示すように、シーケンスチャート３２上の連続した２つのアクションに対して、各アクション名から構成される２ロケーションと、両アクション名から構成されるチャネルを受信する遷移とを両ロケーション間に生成することによって状態遷移履歴通知を認識する。
【００６０】
加えて、observer生成部２２は、図８に示すように、シーケンスチャート３２に含まれる時間に関する要求仕様を有する各アクションに対して、通知される状態遷移履歴が要求仕様を満たす場合にシーケンスチャート３２上の次の状態に遷移可能な遷移を生成するとともに、通知される状態遷移履歴が要求仕様を満たさない場合にエラー状態に遷移する遷移を生成する。
【００６１】
さらに、observer生成部２２は、図８に示すように、シーケンスチャート３２上のアクションに対して、アクション名から構成されるロケーションと初期ロケーションの間に該アクション名から構成されるチャネルを受信する遷移を生成することによって状態遷移履歴がシーケンスから外れたことを認識する。
【００６２】
また、このようなシーケンスチャート３２を入力すると、検証式生成部２３は、図７に示した検証式生成処理に従うことにより、図８に示すような検証式４３を生成する。
【００６３】
次に、図９はobserver生成（時間宣言のケース）および検証式生成を示す模式図である。ここでは、図９に示すようなシーケンスチャート３２が入力された場合の動作例を示す。
【００６４】
入力されたシーケンスチャート３２は、「Process Ａ」という名前のプロセスにおいて、「ReqZeroToruque」という名前のチャネルを受信後、ロケーション「１」のアクションを３００［ｍｓ］以上３２０［ｍｓ］で終了して、「ZeroToruque」という名前のチャネルに送信後、次ロケーションに遷移することを表現している。図８におけるシーケンスチャート３２との違いは、アクションに対する時間制約が“SAduration”という用語で記述されていることであり、この用語は該アクションの実行時間に対する宣言、すなわち、本シーケンスチャート３２に従うある実行例ではこれだけの時間で該アクションが実施されることを意味するものである。このようなシーケンスチャート３２を入力すると、observer生成部２２は、図５および図６に示したobserver生成処理に従うことにより、シーケンスチャート３２が時間に対する要求仕様を含むので、図９に示すようなobserver４２を生成する。
【００６５】
すなわち、observer生成部２２は、図９に示すように、シーケンスチャート３２上の連続した２つのアクションに対して、各アクション名から構成される２ロケーションと、両アクション名から構成されるチャネルを受信する遷移とを両ロケーション間に生成することによって状態遷移履歴通知を認識する。
【００６６】
加えて、observer生成部２２は、図９に示すように、シーケンスチャート３２に含まれる時間に関する宣言を有する各アクションに対して、通知される状態遷移履歴が宣言に合致する場合のみシーケンス上の次の状態に遷移可能な遷移を生成する。
【００６７】
さらに、observer生成部２２は、図９に示すように、シーケンスチャート３２上のアクションに対して、アクション名から構成されるロケーションと初期ロケーションの間に該アクション名から構成されるチャネルを受信する遷移を生成することによって状態遷移履歴がシーケンスから外れたことを認識する。
【００６８】
また、このようなシーケンスチャート３２を入力すると、検証式生成部２３は、図７に示した検証式生成処理に従うことにより、シーケンスチャート３２が時間に対する要求仕様を含まないので、図９に示すような検証式４３を生成する。
【００６９】
次に、遷移抽出イベントが挿入についての複合的な実施例について説明する。ここでは、図１０に示すような状態遷移図３１と、図１１−１および図１１−２に示すような２つのシーケンスチャート３２とが入力されるものとする。図１１−１および図１１−２に示す２つのシーケンスチャート３２は、それぞれ複数のロケーションに対応するアクションを含み、また、どちらも時間に対する要求仕様と時間宣言を含んでいるものとする。
【００７０】
図１１−１のシーケンスチャート３２は、ロケーション１のアクションは最大４００［ｍｓ］で実行されなくてはならないという要求仕様と、ロケーション２のアクションが３００［ｍｓ］〜３５０［ｍｓ］で実行されるという時間宣言を示す。また、図１１−２のシーケンスチャート３２は、ロケーション１のアクションは最大３００［ｍｓ］で実行されなくてはならないという要求仕様と、ロケーション２のアクションが２００［ｍｓ］で実行されるという時間宣言を示す。
【００７１】
上述したような入力例に対する図３に従った遷移抽出イベント挿入の出力結果である修正された状態遷移図を図１２に示し、図５および図６に示したobserver生成処理に従ったobserver生成結果を図１３−１および図１３−２に示し、図７に示した検証式生成処理に従った検証式生成結果を図１４に示す。図１４に示すように、検証式生成部２３は、生成された各observerのエラー状態のロケーションに、いかなる実行パスのいかなる時刻においても、到達しないことを示す検証式４３を生成するとともに、生成された各observerの最後のロケーションに到達する実行パスが存在することを示す検証式４３を生成する。
【００７２】
これら生成された状態遷移４１、observer４２、検証式４３をモデル検査ツール“UPPAAL”で検証すると、図１４に示す検証式４３それぞれに対して、図１５に示す結果が得られる。これから、ロケーション１のアクションは、図１１−１のシーケンスチャート３２に示されるどのような動作でも最大４００［ｍｓ］の要求仕様は満たすが、図１１−２のシーケンスチャート３２に示される最大３００［ｍｓ］の要求仕様は満たしていないことがわかるとともに、図１１−１のシーケンスチャート３２に示される時間での動作は起こりえるが、図１１−２のシーケンスチャート３２に示される時間での動作は起こりえないことがわかる。これらから、入力となった状態遷移は、シーケンスチャート３２に対して矛盾することがわかり、設計に誤りがあることがわかる。
【００７３】
このように本実施の形態によれば、モデル検査に必要な検証式を設計者が作成することなく、かつ、放送型通信チャネルを利用することで元のソフトウェアモデルには影響を与えずに、現実の設計プロセスにおいて作成される複数のシーケンスチャートに記述された要件（時間に対する要求仕様、時間宣言）が用意された状態遷移の設計で満たされるかどうかを検証するモデル検査のために必要な情報が自動生成されるので、モデル検査に精通していない設計者が容易にモデル検査ツールを使いこなすことができる。
【００７４】
［第２の実施の形態］
次に、本発明の第２の実施の形態を図１６ないし図１８に基づいて説明する。なお、前述した第１の実施の形態と同じ部分は同じ符号で示し説明も省略する。
【００７５】
ここで、図１６は本発明の第２の実施の形態にかかるモデル検査用監視オートマトン生成装置１の機能構成を示すブロック図である。図１６に示すように、本実施の形態のモデル検査用監視オートマトン生成装置１は、第１の実施の形態で説明した構成に加えて、observer生成部２２の後段にオブザーバ再入可能化手段であるobserver再入可能化部２４を備えている。
【００７６】
observer再入可能化部２４は、概略的には、シーケンスチャート３２に同一のロケーションが複数回出現する場合に、observer生成部２２で生成されるobserver４２をより正確なものに改良するためのものである。
【００７７】
ここで、observer再入可能化部２４について詳述する。ここで、図１７はobserver再入可能化部２４におけるobserver再入可能化処理の流れを示すフローチャートである。図１７に示すように、observer生成部２２で生成されたobserver４２の全てのロケーションに対して終了していない場合には（ステップＳ６１のＮｏ）、ステップＳ６２に進み、「initロケーションの次ロケーションからの自身に至るロケーション列が、注目しているロケーションの直前までの列と、ロケーション名が同じとなる」様なロケーションが存在するか否かを判断する。
【００７８】
上述したようなロケーションが存在する場合（ステップＳ６２のＹｅｓ）、条件に合うロケーションが複数発見された場合は、注目のロケーションから最も近いロケーションを選択し（ステップＳ６３）、発見したロケーションから、その次の名前を持つロケーションまでの間の遷移とロケーションを保存（単純な遷移か、または、時間に関するguardとclock変数の０クリアを持つ遷移−時間経過０のロケーション−該２ロケーションを名前とするチャネルの受信を行う遷移、の３つ組みとなる。）し（ステップＳ６４）、注目ロケーションから上記次の名前を持つロケーションの間に、保存した遷移とロケーションを追加して（ステップＳ６５）、ステップＳ６１に戻る。
【００７９】
一方、上述したようなロケーションが存在しない場合には（ステップＳ６２のＮｏ）、そのままステップＳ６１に戻る。
【００８０】
このようなステップＳ６１〜Ｓ６５の処理は、observer生成部２２で生成されたobserver４２の全てのロケーションに対して終了したと判断されるまで（ステップＳ６１のＹｅｓ）、繰り返される。
【００８１】
ここで、図１８はobserver再入可能化を示す模式図である。ここでは、図１８に示すようなobserver４２がobserver生成部２２で生成されてobserver再入可能化部２４に入力された場合の動作例を示す。
【００８２】
図１８に示すobserver４２がobserver生成部２２により生成されると、これを入力としたobserver再入可能化部２４は、図１７に示したobserver再入可能化処理に従い、図１８に示すobserver４２´を出力する。図１８に示すobserver４２は、アクション系列「１→２→３→１→２→３→１→２→４」を監視した際に、「１→２→３→１→２→３」の時点で監視すべきシーケンスチャートで無いとされてしまうが、図１８に示すobserver４２´によれば、該アクション系列の後半部分に相当する「１→２→３→１→２→４」を正しく監視できるようになる。
【００８３】
このように本実施の形態によれば、シーケンスチャート３２に同一のロケーションが複数回含まれ、observer４２が該ロケーションを現在の状態と認識している場合に、該ロケーションを遷移元とする状態遷移履歴が通知された際に、シーケンスチャート３２中のより前方に存在する同一名のロケーションも現在状態として認識することができる。
【図面の簡単な説明】
【００８４】
【図１】本発明の第１の実施の形態にかかるモデル検査用監視オートマトン生成装置のハードウェア構成を示すブロック図である。
【図２】モデル検査用監視オートマトン生成装置の機能構成を示すブロック図である。
【図３】遷移抽出イベント挿入部における遷移抽出イベント挿入処理の流れを示すフローチャートである。
【図４】遷移抽出イベントが挿入される状態を示す模式図である。
【図５】observer生成部におけるobserver生成処理の流れを示すフローチャートである。
【図６】observer生成処理の一部の処理の流れを示すフローチャートである。
【図７】検証式生成部における検証式生成処理の流れを示すフローチャートである。
【図８】observer生成（要求仕様のケース）および検証式生成を示す模式図である。
【図９】observer生成（時間宣言のケース）および検証式生成を示す模式図である。
【図１０】入力された状態遷移図の一例を示す模式図である。
【図１１−１】入力されたシーケンスチャートの一例を示す模式図である。
【図１１−２】入力されたシーケンスチャートの一例を示す模式図である。
【図１２】修正された状態遷移図の一例を示す模式図である。
【図１３−１】生成されたobserverの一例を示す模式図である。
【図１３−２】生成されたobserverの一例を示す模式図である。
【図１４】生成された検証式の一例を示す模式図である。
【図１５】モデル検査ツール“UPPAAL”での検証結果の一例を示す模式図である。
【図１６】本発明の第２の実施の形態にかかるモデル検査用監視オートマトン生成装置の機能構成を示すブロック図である。
【図１７】observer再入可能化部におけるobserver再入可能化処理の流れを示すフローチャートである。
【図１８】observer再入可能化を示す模式図である。
【符号の説明】
【００８５】
１      モデル検査用情報生成装置
２１    遷移抽出イベント挿入手段
２２    オブザーバ生成手段
２３    検証式生成手段
２４    オブザーバ再入可能化手段
【図１】
2008021160.tif 000003
【図２】
2008021160.tif 000004
【図３】
2008021160.tif 000005
【図４】
2008021160.tif 000006
【図５】
2008021160.tif 000007
【図６】
2008021160.tif 000008
【図７】
2008021160.tif 000009
【図８】
2008021160.tif 000010
【図９】
2008021160.tif 000011
【図１０】
2008021160.tif 000012
【図１１−１】
2008021160.tif 000013
【図１１−２】
2008021160.tif 000014
【図１２】
2008021160.tif 000015
【図１３−１】
2008021160.tif 000016
【図１３−２】
2008021160.tif 000017
【図１４】
2008021160.tif 000018
【図１５】
2008021160.tif 000019
【図１６】
2008021160.tif 000020
【図１７】
2008021160.tif 000021
【図１８】
2008021160.tif 000022