(57)【要約】【課題】事前に並列プロセス間の関係性の複雑度を予測することを可能とし、モデル検査実施の可否を事前に判断する指針を提供する。【解決手段】各プロセスの状態遷移表データに基づいて、プロセス間通信情報を生成するプロセス間通信情報解析部と、ユーザに並列で動作するプロセスに対応するプロセス間通信情報を選択するように促し、選択されたプロセス間通信情報に外部イベントを合成し、合成後プロセス間通信情報を生成し、プロセス間通信情報及び合成後プロセス間通信情報についてのイベント毎のイベント状態数を算出するプロセス間通信情報入出力部と、前記状態遷移表データにおけるマス数と、前記プロセス間通信情報及び合成後プロセス間通信情報のイベント状態数に基づいて、複雑度を算出する複雑度計算部とを有するモデル検査有効性計測装置。【選択図】図１
2010262365.tif 000002
【特許請求の範囲】
【請求項１】
複雑度の測定対象であるモデルを構成する各プロセスの状態遷移表データに基づいて、プロセス間通信情報を生成する第１の解析手段と、
前記第１の解析手段により生成されたプロセス間通信情報を表示又は提示し、ユーザに並列で動作するプロセスに対応するプロセス間通信情報を選択するように促し、選択されたプロセス間通信情報に外部イベントを合成したプロセス間通信情報である合成後プロセス間通信情報を生成し、プロセス間通信情報及び合成後プロセス間通信情報についてのイベント毎のイベント状態数を算出する第２の解析手段と、
前記状態遷移表データにおけるイベント数と状態数の積であるマス数と、前記プロセス間通信情報及び合成後プロセス間通信情報のイベント状態数に基づいて、複雑度を算出する計算手段と
を有することを特徴とするモデル検査有効性計測装置。
【請求項２】
前記第２の解析手段は、プロセス間通信情報又は合成後プロセス間通信情報において、それが先頭イベントを除いた自己プロセスへの応答イベントを有する場合は、前イベント状態数と応答イベント状態数との積を応答イベントの最終的なイベント状態数として算出する、ことを特徴とする請求項１に記載のモデル検査有効性計測装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査有効性計測装置に関し、より詳しくはプロセス間通信の関係性の抽出及び、これに基づいたモデル検査の有効性を測定する装置であるモデル検査有効性計測装置に関する。
【背景技術】
【０００２】
今日組み込み機器（コンピュータ（マイクロコントローラ）が内部に組み込まれており，そのコンピュータに特定のアプリケーションに特化した処理を行わせる電子装置をいう。例えば、携帯電話や薄型テレビ、DVD／HDDレコーダ、カーナビ、デジタルカメラなど）が普及発展してきている。これら組み込み機器においては、ハードの技術革新により、より一層複雑な制御やアプリケーション機能を機器に組み込むためのニーズが高くなっている。組み込み機器においては、複数の機器が協調して動作する必要があり、機器間の状態とその遷移系列である制御仕様に矛盾がないか確認し、システムを構築する必要がある。
【０００３】
状態遷移モデルに記述された制御仕様において、記述した仕様の正しさを検査するための方法として、モデル検査方法がある。モデル検査方法によれば、状態遷移モデルに対して、考え得る全ての実行系列に対して、デッドロックの検出、特定の条件下における到達／未到達状態の検査が可能となっている。
【０００４】
ただし、このようなモデル検査を実施するためのコストも見過ごせない。実開発以外で検証のためのモデルを作成する必要があるためモデル作成のコストが増加する。また、モデルが作成できても、仕様が複雑である場合や大きい場合は、状態探索木が大きくなり実質探索不可能となり検査結果がでないようなこともある。
【０００５】
このため、全てのシステムに対してモデル検査を実施するのではなく、対象範囲のモデルがモデル検査に向いた問題領域であるかどうかを事前に見積もり、そのコスト対効果を予測して実施する必要性がある。
【０００６】
一般に、モデル検査を実施する場合に、あらかじめ、検査したい状態と、これに対する離散的イベントによる状態遷移モデルを状態遷移表として記述する。記述された状態遷移表のマスの数からある程度のモデルの大きさや複雑度は検討できる。
【０００７】
図２３に、ある状態遷移モデルの状態遷移表の一例を示す。この状態遷移モデルでは、４つの状態Ａ１，Ａ２，Ａ３，Ａ４、及び５つのイベントｅｖ１，ｅｖ２，ｅｖ３，ｅｖ４，ｅｖ５が存在する。この状態遷移表が有するマス数は、状態数（４）×イベント数（５）＝２０となる。このマス数は、モデルの大きさや複雑度を示す指標として使用されることもある。
【０００８】
しかし、このような状態遷移表のマス数による複雑度予測では、１プロセス内での状態とイベントの数だけに依存しており、複数プロセスでのイベントの関係性を考慮できない。複数プロセス間の関係の複雑性は、複数プロセス間のイベントの関係性を見出して検討する必要がある。
【０００９】
状態遷移表のマス数では、複雑度予測が適切に行えない例を以下に示す。ここでは、データを渡すだけのプロトコル（αプロトコルと呼ぶ）と、渡したデータに対して返り値を待つようなプロトコル（βプロトコルと呼ぶ）とを比較して、その複雑度がマス数に基づいて評価できるかどうかを検討する。
【００１０】
図２４は、αプロトコルのシーケンス図である。αプロトコルは、並列プロセスであるＡプロセスとＢプロセスが存在する。ＡプロセスとＢプロセスはまず初期状態となる。つぎに、イベントである時間経過ｔｉｍｅが発生すると、Ａプロセスの状態は、Ｄａｔａ１送信状態となる。Ｄａｔａ１送信状態となったＡプロセスは、アクションとしてＤａｔａ１送信（ＢプロセスにＤａｔａ１を送信する）を実行する。
【００１１】
ＡプロセスからＤａｔａ１を受信したＢプロセスは、その状態を初期状態からＤａｔａ１受信状態に遷移させる。
【００１２】
次に、ＡプロセスはＤａｔａ１送信状態において、イベントであるイベントである時間経過ｔｉｍｅが発生すると、Ａプロセスの状態は、Ｄａｔａ２送信状態に遷移する。Ｄａｔａ２送信状態となったＡプロセスは、アクションとしてＤａｔａ２送信（ＢプロセスにＤａｔａ２を送信する）を実行する。
【００１３】
ＡプロセスからＤａｔａ２を受信したＢプロセスは、その状態をＤａｔａ１受信状態からＤａｔａ２受信状態に遷移させる。
【００１４】
上記Ａプロセスの状態遷移表を図２５に掲げる。図示のようにＡプロセスの状態遷移表のマス数は「３」である。また、上記Ｂプロセスの状態遷移表を図２６に掲げる。図示のようにＢプロセスの状態遷移表のマス数は「６」である。すなわち、図２４に示す非同期通信応答無しのプロトコルの複雑度を示す指標であるマス数は「３」＋「６」＝９となる。
【００１５】
図２４のαプロトコルの対比例として、非同期通信応答待ちの通信プロトコルであるβプロトコルのシーケンス図を図２７に掲げる。
【００１６】
βプロトコルは、並列プロセスであるＡ’プロセスとＢ’プロセスで構成されている。Ａ’プロセスとＢ’プロセスはまず初期状態となる。つぎに、イベントである時間経過ｔｉｍｅが発生すると、Ａ’プロセスの状態は、ｒｅａｄｙ送信状態に遷移する。ｒｅａｄｙ送信状態となったＡ’プロセスは、アクションとしてｒｅａｄｙ送信（Ｂプロセスにｒｅａｄｙメッセージを送信する）を実行する。
【００１７】
Ａ’プロセスからｒｅａｄｙメッセージを受信したＢ’プロセスは、その状態を初期状態からｒｅａｄｙ受信状態に遷移させる。次に、ｒｅａｄｙ受信状態となったＢ’プロセスは、アクションとしてｏｋ送信（Ａ’プロセスにｏｋメッセージを送信する）を実行する。
【００１８】
Ｂ’プロセスからｏｋメッセージを受信したＡ’プロセスは、その状態をｒｅａｄｙ送信状態からｏｋ受信状態に遷移させる。
【００１９】
上記Ａ’プロセスの状態遷移表を図２８に掲げる。図示のようにＡ’プロセスの状態遷移表のマス数は「６」である。また、上記Ｂ’プロセスの状態遷移表を図２９に掲げる。図示のようにＢ’プロセスの状態遷移表のマス数は「２」である。すなわち、図２７に示す非同期通信応答待ちの通信プロトコルであるβプロトコルの複雑度を示す指標であるマス数は「６」＋「２」＝８となる。
【００２０】
上述の２つの通信プロトコル、αプロトコルとβプロトコルを比較すると、αプロトコルはデータを渡すだけの単純なプロトコルであるのに対し、βプロトコルは、渡したデータに対して返り値を待つような、αプロトコルに比較して複雑なプロトコルである。しかし、両者の状態遷移表のマス数では「９」と「８」で大差がない。このように、通信プロトコルにおける特性は、状態遷移表のマス数からだけでは読み取ることができない。
【００２１】
一般に、モデル検査の有効性を事前に予測するような従来技術は存在しないが、有効性を予測するために利用する技術である、状態遷移表からプロセス間通信情報への変換に関しては類似技術は存在する（特許文献１）。この従来技術は、状態遷移表ベースで記述された通信プロトコル仕様をもとに、データ伝送制御シーケンス図を自動的に作成する方法であって、自プロセスの状態遷移表をもとに、自プロセスと相手プロセスのデータ通信関係を、相手プロセスからのイベントをユーザが順次与えることによって、データ伝送制御シーケンス図を自動的に作成していくものである。
【先行技術文献】
【特許文献】
【００２２】
【特許文献１】特開平３−９１８５５号公開公報
【発明の概要】
【発明が解決しようとする課題】
【００２３】
上述のように、従来の技術では、対象範囲のモデルがモデル検査に向いた問題領域であるかどうかを事前に見積もり、そのコスト対効果を予測して実施することができなかった。
【００２４】
本発明の目的は、事前に並列プロセス間の関係性の複雑度を予測することを可能とし、これにより検査条件が並列プロセスの状態に関するものである場合、モデル検査実施の可否を事前に判断する指針（指標、判断材料）を提供することを目的としている。
【００２５】
なお、本特許では、状態遷移表からプロセス間通信情報を算出するが、状態遷移表から自動的に算出できる範囲で生成させる。自動的に算出できる範囲とは、自プロセス内でのイベントに対して、相手プロセスへデータが送信され、相手プロセスでデータが受信され、さらにそれに対して、相手プロセスから自プロセスにデータが送信されるという連続した範囲である。
【課題を解決するための手段】
【００２６】
上記課題を解決するための手段として、本発明は以下の特徴を有する。
【００２７】
本発明は、複雑度の測定対象であるモデルを構成する各プロセスの状態遷移表データに基づいて、プロセス間通信情報を生成する第１の解析手段と、前記第１の解析手段により生成されたプロセス間通信情報を表示又は提示し、ユーザに並列で動作するプロセスに対応するプロセス間通信情報を選択するように促し、選択されたプロセス間通信情報に外部イベントを合成したプロセス間通信情報である合成後プロセス間通信情報を生成し、プロセス間通信情報及び合成後プロセス間通信情報についてのイベント毎のイベント状態数を算出する第２の解析手段と、前記状態遷移表データにおけるイベント数と状態数の積であるマス数と、前記プロセス間通信情報及び合成後プロセス間通信情報のイベント状態数に基づいて、複雑度を算出する計算手段とを有することを特徴としている。
【発明の効果】
【００２８】
本発明によれば、事前に並列プロセス間の関係性の複雑度を予測することを可能とし、これにより検査条件が並列プロセスの状態に関するものである場合、モデル検査実施の可否又は適否を事前に判断する指針（指標、判断材料）を提供する事が可能となる。
【発明を実施するための最良の形態】
【００２９】
以下、図面を参照しながら本発明の実施の形態を説明する。
【００３０】
［１．概要］
本発明は、モデル検査の入力となる仕様を状態遷移表でモデル検査有効性計測装置に入力することを前提としている。モデル検査有効性計測装置は、入力された状態遷移表から、プロセス間の通信に関係する情報（プロセス間通信情報と呼ぶ）を抽出し、抽出されたプロセス間の通信の複雑度を、モデル検査の観点から計算することで、検査対象であるモデルの複雑度を予測し、モデル検査実施のための指針とする。
【００３１】
これを実現するための方法として、本発明は以下の2つの技術を用いる。
【００３２】
＜技術１＞  状態遷移表からプロセス間通信情報への変換規則
有効性評価の対象であるモデルを構成する各プロセスの状態遷移表をもとに、プロセス間の関係性をプロセス間通信情報として記述する。プロセス間通信情報は例えば、以下のような形態で記述されたデータである
「例」：        (A:ev1,B:gev1,C:gev2,A,B:gev3)
＜技術２＞  プロセス間通信情報の複雑度計算
上記のプロセス間通信情報から、プロセス間の関係性を並列性と応答性とをもとに、複雑度を計算する。
【００３３】
［１．モデル検査有効性計測装置の構成］
本実施の形態は、モデル検査有効性計測装置（以下、「計測装置」と略す）として提案される。モデル検査有効性計測装置は、上記技術１，技術２を用いて対象範囲のモデルがモデル検査に向いた問題領域であるかどうかを事前に見積もるための指針である複雑度を出力する装置である。
【００３４】
本実施の形態にかかる計測装置は、例えばコンピュータ、ワークステーションなどの情報処理装置によって実現される装置である。この情報処理装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、入出力装置（Ｉ／Ｏ）、及び必要な場合にはハードディスク装置等の外部記憶装置を具備している装置である。
【００３５】
図１に、計測装置の構成例を示した機能ブロック図を掲げる。計測装置１は、複雑度の測定対象であるモデルを構成する各プロセスの状態遷移表データ２を入力として受け取るプロセス間通信情報解析部１０と、プロセス間通信情報解析部１０に接続されたプロセス間通信情報格納部２０と、プロセス間通信情報格納部２０に接続されたプロセス間通信情報入出力部３０と、プロセス間通信情報入出力部３０に接続された並列動作可能入力部４０と、プロセス間通信情報解析部１０及びプロセス間通信情報格納部２０に接続された複雑度計算部５０と、複雑度計算部５０に接続された複雑度表示部６０とを有している。
【００３６】
なお、ここで「接続」とは、物理的に結合されている状態に限られず、データの受け渡しが可能である状態を含む意味である。また、上記の各構成要素はＣＰＵ及びＣＰＵによって実行されるプログラムによって実現される機能に対応するものであり、実際に各構成要素に対応するハードウエアを計測装置１が備えている必要はない。
【００３７】
以下、計測装置１の各構成要素について説明する。  
【００３８】
［１．１．プロセス間通信情報解析部］
本発明の第１の解析手段に相当するプロセス間通信情報解析部１０は、各プロセスの状態遷移表データ２を解析し、プロセス間通信情報を生成する。「プロセス間通信情報」は、本計測装置１が、複雑度を計算するためのデータである。プロセス間通信情報の詳細及び具体例については後述する。
【００３９】
プロセス間通信情報解析部１０は、作成したプロセス間通信情報を、プロセス間通信情報格納部２に渡し、格納させる。
【００４０】
また、プロセス間通信情報解析部１０は、状態遷移表データ２から、当該状態遷移表のマス数を算出し、これをプロセス間通信情報格納部２０に記憶させる。
【００４１】
［１．２．プロセス間通信情報格納部］
プロセス間通信情報格納部２０は、プロセス間通信情報解析部で生成されたプロセス間通信情報を格納する機能を有する。また、後述するプロセス間通信情報入出力部３０により生成された、外部イベントが合成されたプロセス間通信情報を格納する機能を有する。
【００４２】
［１．３．プロセス間通信情報入出力部］
本発明の第２の解析手段に相当するプロセス間通信情報入出力部３０は、プロセス間通信情報格納部２０に格納されているプロセス間通信情報を文字や図形式など適宜の形式で表示又は提示する機能を有する。プロセス間通信情報入出力部３０は、プロセス間通信情報を文字や図形式で表示し、ユーザ（計測装置１の使用者、オペレータなど）にプロセス間通信情報のうち、並列で動作するプロセスに対応するプロセス間通信情報を選択するように促す。ユーザは、表示又は提示されたプロセス間通信情報から、並列で動作するプロセスに対応するプロセス間通信情報を指定する。この指定には、キーボード、ポインティングデバイスなどの入力装置をユーザが使用することなどによって行われればよい。
【００４３】
プロセス間通信情報入出力部３０は、並列で動作するプロセス間通信情報がユーザによって指定された場合、それらの関係に基づいて、プロセス間通信情報に外部イベントを合成したプロセス間通信情報（以下、「合成後プロセス間通信情報」と呼ぶ）を生成する。
【００４４】
プロセス間通信情報入出力部３０は、合成後プロセス間通信情報に基づいて、そのプロセス間通信情報における、外部イベントを合成した結果得られるイベント毎のイベント状態数を算出する。
【００４５】
プロセス間通信情報入出力部３０は、合成後プロセス間通信情報、及びプロセス間通信情報毎のイベント状態数の和をプロセス間通信情報格納部２０に登録する。
【００４６】
［１．４．並列動作可能入力部］
並列動作可能入力部４０は、プロセス間通信情報入出力部３０によって表示又は提示されたプロセス間通信情報のうち、並列で動作するプロセスに対応するプロセス間通信情報をユーザに指定させる機能を有する。この指定は、キーボード、ポインティングデバイスなどの入力装置をユーザが使用することなどによって行われればよい。
【００４７】
［１．５．複雑度計算部］
本発明の計算手段に相当する複雑度計算部５０は、プロセス間通信情報格納部２０に登録されている状態遷移表のマス数及び、プロセス間通信情報及び／又は合成後プロセス間通信情報のイベント状態数から複雑度を算出する機能を有する。
【００４８】
なお、「複雑度」は、イベント状態数の和を状態遷移表のマス数で割った値である。
【００４９】
［１．６．複雑度表示部］
複雑度表示部６０は、複雑度計算部５０による算出した値、又はこの値に基づいたモデル検査有効性の指標を表示又は提示する機能を有する。表示又は提示の形態、態様、方式は、どのようなものであってもかまわない。例えば、数値そのものを表示、印刷等する態様でも良いし、数字に応じたメッセージ（例えば、適合、不適合、不可、など）の表示、印刷等であってもかまわない。
【００５０】
［２．動作例］
次に、計測装置１の動作例について説明する。  
【００５１】
以下、本計測装置１の動作例を説明するため、複雑度の測定対象となるシステムを用いる。このシステムは、Ａプロセス、Ｂプロセス、Ｃプロセスの３つのプロセスからなる。図２にＡプロセスの状態遷移図を示し、図３にＢプロセスの状態遷移図を示し、図４にＣプロセスの状態遷移図を示す。図２から図４において、「イベント名／プロセス名：グローバルイベント名」の形式で表示されているのは、イベント名で示されたイベントが発生したときに、プロセス名で示されたプロセスに送信するグローバルイベントが発生することを意味している。
【００５２】
まず、ユーザは、複雑度の測定対象である、並列プロセスで動作するシステムについて、当該システムを構成する各プロセスの状態遷移表のデータ（状態遷移表データと呼ぶ）を用意する。状態遷移表データ２は、ユーザが予め用意しておき、この時、並列プロセスで共有するデータ、もしくは通信イベントは、状態遷移表上にグローバルイベント(gev)として定義する。すなわち、グローバルイベントは、他プロセスのデータを共有メモリやメッセージ通信といったなんらかの方法で参照するイベントであり、これに対してローカルイベントは、他プロセスとは関係なく、ユーザからの入力や、エラーイベントのようにランダムに発生するイベントをいい、状態遷移表データ２中では、「ｅｖ」のように標記する。
【００５３】
状態遷移表データ２において、グローバルイベントを他プロセスに発行する場合には、該当するマスのアクション欄にグローバルイベントの発行を明示する。このとき、発行先の対象プロセスを明記する。本実施の形態では、対象となるマスのアクション欄に「発行先プロセス名：グローバルイベント名」という形式でグローバルイベントの発行が記述される。例えば、Ｂプロセスに「ｇｅｖ１」というグローバルイベントを発行する場合には、該当するマスのアクション欄に「Ｂ：ｇｅｖ１」と記述されることになる。
【００５４】
図５から図７に、本計測装置１に入力するために用意された状態遷移表データ２の例を示す。図５は、上述のＡプロセスについての状態遷移表データを示した図であり、図６は、上述のＢプロセスについての状態遷移表データを示した図であり、図７は、上述のＣプロセスについての状態遷移表データを示した図である。それぞれの状態遷移表データ２は、グローバルイベントに対応する列を有している。
【００５５】
なお、図７において、「Ａ，Ｂ：ｇｅｖ２」とする記述は、Ａプロセス及びＢプロセスを発行先とするグローバルイベント「ｇｅｖ２」が発行されることを意味している。
【００５６】
（２）上記状態遷移表データ２は、ユーザによって計測装置１に入力される。入力された状態遷移表データ２は、プロセス間通信情報解析部１０によって受け取られる。プロセス間通信情報解析部１０は、受け取った状態遷移表データ２を処理する。図８は、プロセス間通信情報解析部１０が状態遷移表データ２を処理する処理内容の一例を示したフローチャート、図９は、図８のフローチャートに続くフローチャートである。以下、図８及び図９を参照しながらプロセス間通信情報解析部１０の動作（処理）について説明する。
【００５７】
まず、前述のように複雑度の測定対象となるシステムを構成する各プロセスについて、状態遷移表データ２を準備し、この状態遷移表データ２をプロセス間通信情報解析部１０に入力する（Ｓ１０）。状態遷移表データ２を受け取ったプロセス間通信情報解析部１０は、一つのプロセスについての状態遷移表データ２の一行の内容を読み込む（Ｓ２０）。
【００５８】
プロセス間通信情報解析部１０は、Ｓ２０において読み込んだ行に含まれるマスのうち、一つのマスを特定し、そのマスのアクションの欄にグローバルイベント（記号：ｇｅｖ）が含まれるか否かを判定する（Ｓ３０）。
【００５９】
このステップＳ３０においてグローバルイベント（記号：ｇｅｖ）が含まれないと判定した場合、プロセス間通信情報解析部１０は、直前のＳ２０において読み込んだ行の全てのマスについてＳ３０の判定を行ったか否かを判定する（Ｓ５０）。一方、このステップＳ３０においてグローバルイベント（記号：ｇｅｖ）が含まれていると判定した場合、プロセス間通信情報解析部１０は、そのマスの列に対応するイベントと、アクションをプロセス間通信情報として抽出する。
【００６０】
例えば、図５に示したＡプロセスの状態遷移表データ２からは、以下のプロセス間通信情報（以下、プロセス通信情報Ａと呼ぶ）が生成される。
【００６１】
（Ａ：ｅｖ１、Ｂ：ｇｅｖ１）
また、図６に示したＢプロセスの状態遷移表データ２からは、以下のプロセス間通信情報（以下、プロセス通信情報Ｂと呼ぶ）が生成される。
【００６２】
（Ｂ：ｇｅｖ１、Ｃ：ｇｅｖ２）
また、図７に示したＣプロセスの状態遷移表データ２からは、以下のプロセス間通信情報（以下、プロセス通信情報Ｃと呼ぶ）が生成される。
【００６３】
（Ｃ：ｇｅｖ２、Ａ，Ｂ：ｇｅｖ３）
図８に戻り、プロセス間通信情報解析部１０の動作例（処理）の説明を続ける。  
【００６４】
ステップＳ５０に制御が移ると、プロセス間通信情報解析部１０は、現在の処理対象行の全てのマスについてＳ３０の判定を行ったか否かを判定する（Ｓ５０）。対象行全てのマスについてＳ３０の判定を行っていないと判定した場合（Ｓ５０，Ｎｏ）は、プロセス間通信情報解析部１０はＳ３０に戻り、未処理のマスについてＳ３０，Ｓ４０の処理を実行する。一方、Ｓ５０において全てのマスについてＳ３０の判定を行ったと判定した場合（Ｓ５０、Ｙｅｓ）は、プロセス間通信情報解析部１０は現在の処理対象の状態遷移表データ２の全ての行についてＳ２０からＳ５０の処理を行ったか否かを判定する（Ｓ６０）。対象状態遷移表データ２の全ての行についてＳ２０からＳ５０の処理を行っていないと判定した場合（Ｓ６０，Ｎｏ）は、プロセス間通信情報解析部１０はＳ２０に戻り、未処理の行についてＳ３０からＳ５０の処理を実行する。一方、Ｓ６０において全ての行についてＳＳ３０からＳ５０の処理を行ったと判定した場合（Ｓ６０、Ｙｅｓ）は、その状態遷移表データ２のマス数として、その状態遷移表データ２におけるグローバルイベント及びグローバルイベント以外の抽出イベントの数をイベント数として、そのイベント数と状態数の積をマス数として記憶保持する（Ｓ７０）。
【００６５】
次に、プロセス間通信情報解析部１０は、Ｓ１０において入力された全ての状態遷移表データ２について、Ｓ２０からＳ７０の処理を実行したか否かを判定する（Ｓ８０）。全ての全ての状態遷移表データ２についてはＳ２０からＳ７０の処理を実行していないと判定した場合（Ｓ８０，Ｎｏ）、プロセス間通信情報解析部１０は、Ｓ１０に戻り、未処理の状態遷移表データ２の入力受付を行う（Ｓ１０）。一方、複雑度の測定対象であるシステムについて、全ての状態遷移表データ２についてＳ２０からＳ７０の処理を実行したと判定した場合（Ｓ８０，Ｙｅｓ）、プロセス間通信情報解析部１０は、Ｓ７０にて記憶保持した、各状態遷移表データ２についてのマス数の合計を算出し、算出した値を、測定対象であるシステムの状態遷移表マス数として、プロセス間通信情報格納部２０に記憶させる（図９，Ｓ９０）。
【００６６】
次に、プロセス間通信情報解析部１０は、Ｓ４０において抽出したプロセス間通信情報を読み出す（Ｓ１００）。プロセス間通信情報解析部１０は、読み出したプロセス間通信情報の先頭が通常イベント（ローカルイベント）であるプロセス間通信情報があるか否かを判定する（Ｓ１１０）。先頭が通常イベントであるプロセス間通信情報がないと判定した場合（Ｓ１１０，Ｎｏ）は、後述するＳ１６０に進む。一方、先頭が通常イベントであるプロセス間通信情報があると判定した場合（Ｓ１１０，Ｙｅｓ）、プロセス間通信情報解析部１０は、先頭が通常イベントであるプロセス間通信情報を読み込む（Ｓ１２０）。次に、ロセス間通信情報解析部１０は、送信先プロセスのプロセス間通信情報において、先頭が送信元のグローバルイベントと同じである別のプロセス間通信情報を探索する（Ｓ１３０）。言い換えれば、Ｓ１２０において読み込まれたプロセス間通信情報の出力イベントと、同じグローバルイベントを、入力イベントとして持つプロセス間通信情報を探索する。
【００６７】
プロセス間通信情報解析部１０は、Ｓ１３０で探索した結果そのようなプロセス間通信情報があるか否かを判定する（Ｓ１４０）。そのようなプロセス間通信情報がないと判定した場合（Ｓ１４０，Ｎｏ）は、Ｓ１１０に戻り別のプロセス間通信情報についてＳ１１０からＳ１４０の処理を行う。一方、そのようなプロセス間通信情報があると判定した場合（Ｓ１４０，Ｙｅｓ）は、直近のＳ１２０で読み込まれたプロセス間通信情報と、直近のＳ１３０によって探索されたプロセス間通信情報とを合成し、新たなプロセス間通信情報（合成後プロセス通信情報と呼ぶ）を生成する（Ｓ１５０）。「合成」は、一方のプロセス間通信情報における出力イベントが、他のプロセス間通信情報における入力イベントと同一である場合、この出力イベントと入力イベントとシーケンシャルなイベントとしてイベント同士を結合するように、合成後プロセス間通信情報を生成することをいう。
【００６８】
前述のＡプロセス、Ｂプロセス、Ｃプロセスを例に取ると、Ａプロセスのプロセス間通信情報は（Ａ：ｅｖ１、Ｂ：ｇｅｖ１）であり、Ｂプロセスのプロセス間通信情報は（Ｂ：ｇｅｖ１、Ｃ：ｇｅｖ２）であった。前者のプロセス間通信情報の出力イベントはｇｅｖ１であり、後者のプロセス間通信情報の入力イベントはｇｅｖ１である。よって、これらプロセス間通信情報から、合成されたプロセス間通信情報（Ａ：ｅｖ１、Ｂ：ｇｅｖ１、Ｃ：ｇｅｖ２）が生成される。
【００６９】
さらに、この合成されたプロセス間通信情報（Ａ：ｅｖ１、Ｂ：ｇｅｖ１、Ｃ：ｇｅｖ２）と、Ｃプロセスのプロセス間通信情報（Ｃ：ｇｅｖ２、Ａ，Ｂ：ｇｅｖ３）との間において、前者の出力イベントと後者の入力イベントは同一であるため、これらプロセス間通信情報もさらに合成され、（Ａ：ｅｖ１、Ｂ：ｇｅｖ１、Ｃ：ｇｅｖ２、Ａ，Ｂ：ｇｅｖ３）という合成後プロセス間通信情報が最終的に得られることになる。
【００７０】
図９に戻り、フローチャートの説明を続ける。Ｓ１５０の後、プロセス間通信情報解析部１０は、全てのプロセス間通信情報についてＳ１１０からＳ１５０の処理を行ったか否かを判定する（Ｓ１６０）。全てのプロセス間通信情報についてＳ１１０からＳ１５０の処理を行っていないと判定した場合（Ｓ１６０，Ｎｏ）、プロセス間通信情報解析部１０は、Ｓ１１０に戻りプロセス間通信情報の合成を続行する。一方、全てのプロセス間通信情報についてＳ１１０からＳ１５０の処理を行ったと判定した場合（Ｓ１６０，Ｙｅｓ）、プロセス間通信情報解析部１０は、Ｓ１５０において生成した合成後プロセス間通信情報をプロセス間通信情報格納部２０に登録させて、処理を終了する（Ｓ１７０）。
【００７１】
上述のＳ１７０後の計測装置１の動作例（処理）について、図１０，図１１を参照しながら説明する。図１０は、Ｓ１７０後の計測装置１の動作例（処理）を示すフローチャート、図１１は図１０に続くフローチャートである。
【００７２】
Ｓ１７０の後、計測装置１、より詳しくはプロセス間通信情報入出力部３０は、プロセス間通信情報格納部２０に格納されているプロセス間通信情報（合成後プロセス間通信情報を含む）を文字や図形式など適宜の形式で表示又は提示し、プロセス間通信情報が同時に動作する（並列動作する）プロセス間通信情報同士をユーザに指定するよう促す（Ｓ２１０）。ユーザは、並列動作可能入力部４０を用いて、並列で動作するプロセスに対応するプロセス間通信情報を指定する。ユーザは、別プロセスに置いて同時に起動可能なプロセス間通信同士を並列実行可能性があるプロセス間通信情報として指定する。抽出のポイントは、プロセス間通信情報の開始イベント開始状態を参照し、システムにおいて同時に起こりうるか否かを判断することにより行う。
【００７３】
非同期通信の場合、応答性に加え並列で動作することにより、メッセージクロスのような問題が発生しやすい。同時に実行可能なプロセス間通信情報を洗い出すことにより、各プロセスが通信時に発生しうるグローバルイベントを全て洗い出すことが出来る。
【００７４】
並列で動作するプロセスに対応するプロセス間通信情報の例を挙げる。図１２（Ａ）（Ｂ）は、Ｘプロセス、Ｙプロセスの状態遷移図である。これらＸプロセス及びＹプロセスの合成後プロセス間通信情報は、（Ｘ：ｔｉｍｅ，Ｙ：ｒｅａｄｙ；Ｘ：ＯＫ）および（Ｙ：ｔｉｍｅ，Ｘ：ｒｅａｄｙ；Ｙ：ＯＫ）となる。これらプロセス間通信情報は、Ｘプロセス、Ｙプロセスとも初期状態からｔｉｍｅイベントにより起動されるため、同時実行可能といえる。
【００７５】
図１０に戻り、計測装置１の動作の説明を続ける。
【００７６】
次に、計測装置１、より詳しくは複雑度計算部５０は、ユーザによって指定された同時に動作するプロセス間通信情報において、外部イベントを挿入したプロセス間通信情報を生成する（Ｓ２３０）。より詳しくは、複雑度計算部５０は、並列実行可能なプロセス間通信情報同士について、グローバルイベントを送信中に、別のグローバルイベントが到達する可能性を考慮してプロセス間通信情報に外部イベントを挿入する（Ｓ２３０）。
【００７７】
図１２に示したＸプロセス、Ｙプロセスを例として、Ｓ２３０によって行われるプロセス間通信情報に外部イベントを挿入して、別のグローバルイベントが到達する可能性を考慮したプロセス間通信情報を生成する例を説明する。
【００７８】
図１２（Ａ）のＸプロセスにおいて、Ｘプロセスがｒｅａｄｙを送信してからＹプロセスがｒｅａｄｙ受信するまでに、ＸプロセスもＹプロセスから送信されたｒｅａｄｙを受信する可能性がある。Ｙプロセスは、Ｘプロセスがｒｅａｄｙ送信状態又はｒｅａｄｙ受信状態になる事を考慮する。
【００７９】
また、Ｙプロセスからｏｋを送信した後Ｘプロセスがｏｋを受信するまでに、Ｙプロセスもｏｋを受信する可能性がある。従って、ＸプロセスはＹプロセスがｒｅａｄｙ受信状態又はｏｋ受信状態になることを考慮する。
【００８０】
Ｘプロセスのプロセス間通信情報（Ｘ：ｔｉｍｅ，Ｙ：ｒｅａｄｙ；Ｘ：ＯＫ）において、Ｙプロセス送信時には、Ｘプロセスへの送信情報を挿入し、Ｘプロセスの送信時にはＹプロセスの送信情報を挿入する。この場合には、
（Ｘ：ｔｉｍｅ，Ｙ：ｒｅａｄｙ（Ｘ：ｒｅａｄｙ）；Ｘ：ｏｋ（Ｙ：ｏｋ））
というプロセス間通信情報が生成されることになる。
【００８１】
一方、Ｙプロセスのプロセス間通信情報（Ｙ：ｔｉｍｅ，Ｘ：ｒｅａｄｙ；Ｙ：ＯＫ）において、Ａプロセス送信時には、Ｙプロセスへの送信情報を挿入し、Ｙプロセスの送信時にはＸプロセスの送信情報を挿入する。この場合には、
（Ｙ：ｔｉｍｅ，Ｘ：ｒｅａｄｙ（Ｙ：ｒｅａｄｙ）；Ｙ：ｏｋ（Ｘ：ｏｋ））
というプロセス間通信情報が生成されることになる。図１３に、並列動作可能性を考慮した場合のＸ、Ｙプロセスの状態遷移図を示す。
【００８２】
図１０に戻り、計測装置１の動作例の説明を続ける。
【００８３】
次に、複雑度計算部５０は、各プロセス間通信情報のイベント状態数を決定し、決定したイベント状態数をプロセス間通信情報格納部２０に登録する。
【００８４】
「イベント状態数」は、送信イベントの数と外部イベントの数の和である。具体的には、複雑度計算部５０は、同時起動により送信時に外部イベントが発生する可能性があるプロセス間通信情報を抽出する。プロセス間通信情報において、送信イベントに対してかっこ（）内に表しているものが送信時に発生する可能性がある外部イベントである。
【００８５】
例を挙げて説明する。図１４は先に示したＸプロセス、Ｙプロセスのプロセス間通信情報であって、外部イベントが挿入されたプロセス間通信情報である。図１４（Ａ）はＸプロセスについての、外部イベントが挿入されたプロセス間通信情報であり、図１４（Ｂ）はＹプロセスについての、外部イベントが挿入されたプロセス間通信情報である。いずれのプロセス間通信情報についても、イベント状態数は、２状態＋２状態＝４状態で、イベント状態数は４となる。
【００８６】
上記ステップＳ２４０に続いて、複雑度計算部５０は、プロセス間通信情報での応答性を考慮するための処理を行う。「応答性」とは、プロセス間通信情報において、例えばreadyを送信後に、ok受信待ちをするような、一方が送信したメッセージに応答するメッセージが返されることことをいう 。応答性は、応答待ちまでの状態がいくつに分かれるかに依存する。
【００８７】
次に、図１１を参照しながら上述Ｓ２４０以降の処理について説明する。  
【００８８】
まず、複雑度計算部５０は、プロセス間通信情報格納部２０から、プロセス間通信情報を読み出す。この読み出されたプロセス間通信情報は、外部イベントが挿入されたプロセス間通信情報である。
【００８９】
次に、複雑度計算部５０は、読み出したプロセス間通信情報において、先頭イベントを除いた自己プロセスへの応答イベントを検索する（Ｓ２６０）。複雑度計算部５０は、検索の結果、応答イベントがあるか否かを判定する（Ｓ２７０）。応答イベントがないと判定した場合（Ｓ２７０，Ｎｏ）、複雑度計算部５０は、後述するＳ３００に制御を移す。一方、応答イベントがあると判定した場合（Ｓ２７０，Ｙｅｓ）、複雑度計算部５０は、前イベント状態数と応答イベント状態数との積を応答イベントの最終的なイベント状態数として、プロセス間通信情報格納部２０に登録する（Ｓ２８０）。なお、応答イベント状態数は、応答イベントの前のイベント状態数（前イベント状態数という）に応答イベントの状態数をかけた値が、応答イベントの最終的なイベント状態数（応答イベント状態数と呼ぶ）になる。図１５に、先に示したＸプロセス、Ｙプロセスのプロセス間通信情報における応答イベント状態数を示す。
【００９０】
次に、複雑度計算部５０は、そのプロセス間通信情報についての全イベント状態数をそのプロセス間通信情報に対応する状態遷移表データのマス数で割った値を求め、その値をそのプロセス間通信情報の複雑度としてプロセス間通信情報格納部２０に登録する（Ｓ２９０）。なお、全イベント状態数は、Ｓ２４０において求めたイベント状態数と、Ｓ２８０において求めた応答イベントの最終的なイベント状態数の和である。
【００９１】
次に、複雑度計算部５０は、プロセス間通信情報格納部２０に登録されているすべてのプロセス間通信情報について、Ｓ２６０からＳ２９０を行ったか否かを判定する（Ｓ３００）。すべてのプロセス間通信情報について上記処理を行っている場合（Ｓ３００，Ｙｅｓ）は処理を終了し、すべてのプロセス間通信情報について上記処理を行っていない場合（Ｓ３００、Ｎｏ）、ステップＳ２５０に戻り、残りのプロセス間通信情報についてＳ２６０からＳ２９０を実行する。
【００９２】
以上で、計測装置１の動作例（処理）の説明を終了する。
【００９３】
［３．複雑度の測定例］
本実施の形態にかかる計測装置１による複雑度の測定例を示す。
（１）通信プロトコル間に同時起動可能なプロトコルがない場合
図１６に、通信プロトコル間に同時起動可能なプロトコルがない場合のシステムについて、状態遷移図をしめす。このシステムは、ａプロセスとｂプロセスで構成されている。図１７に、図１６に示したａプロセスとｂプロセスで構成されるシステムの状態遷移表を示す。このシステムを計測装置１でその複雑度を測定すると、イベント状態数は２，マス数は１５であり、従って複雑度＝イベント状態数／マス数＝２／１５＝０．１３となる。
【００９４】
（２）通信プロトコル間の一方が同時起動可能なプロトコルである場合
図１８に、通信プロトコル間の一方が同時起動可能なプロトコルがである場合のシステムについて、状態遷移図をしめす。このシステムは、ａ’プロセスとｂ’プロセスで構成されている。図１９に、図１８に示したａ’プロセスとｂ’プロセスで構成されるシステムの状態遷移表を示す。このシステムを計測装置１でその複雑度を測定すると、イベント状態数は８，マス数は１５であり、従って複雑度＝イベント状態数／マス数＝８／１５＝０．５３となる。
【００９５】
（３）通信プロトコル間の双方が同時起動可能なプロトコルである場合
図２０に、通信プロトコル間の双方が同時起動可能なプロトコルがである場合のシステムについて、状態遷移図をしめす。このシステムは、ａ’’プロセスとｂ’’プロセスで構成されている。図２１に、図２０に示したａ’’プロセスとｂ’’プロセスで構成されるシステムの状態遷移表を示す。このシステムを計測装置１でその複雑度を測定すると、イベント状態数は１２，マス数は１２であり、従って複雑度＝イベント状態数／マス数＝１２／１２＝１となる。
【００９６】
［４．複雑度の評価］
次に、計測装置１により出力された複雑度の値に基づいて、測定対象となるシステムのモデル検査についてどのように評価するかを説明する。
【００９７】
図２２に、複雑度と、プロセス間関係性、モデル検査意義、モデル検査の有効性との関係を示す表の例を掲げる。この例に示した表は、複雑度の値によって３つのカテゴリに分類し、それぞれのカテゴリについてプロセス間関係性、モデル検査意義、モデル検査の有効性についてコメントしている。ただし、この表の内容及びカテゴリの分類は、あくまで一例であり本発明の技術的範囲がこの基準に限定される趣旨ではない。
【００９８】
［５．まとめ］
本発明によれば、状態遷移表で表されたプロセス単独の仕様からプロセス間の通信プロトコルであるプロセス間通信情報を導きだすことができ、非同期通信で問題となりがちな、応答性と並列性に着目しプロセス間の関係性の複雑度を定義することができ、定義される非同期通信の複雑度から、どのような側面でのモデル検査が有効であるかを事前に予測できる。
【図面の簡単な説明】
【００９９】
【図１】本発明の実施の形態にかかる計測装置の構成例を示した機能ブロック図
【図２】Aプロセスの状態遷移図
【図３】Ｂプロセスの状態遷移図
【図４】Ｃプロセスの状態遷移図
【図５】Ａプロセスについての状態遷移表データを示す図
【図６】Ｂプロセスについての状態遷移表データを示す図
【図７】Ｃプロセスについての状態遷移表データを示す図
【図８】プロセス間通信情報解析部が状態遷移表データ２を処理する処理内容の一例を示したフローチャート
【図９】図８のフローチャートに続くフローチャート
【図１０】Ｓ１７０後の計測装置の動作例（処理）を示すフローチャート、
【図１１】図１０に続くフローチャート
【図１２】（Ａ）はＸプロセスの状態遷移図、（Ｂ）はＹプロセスの状態遷移図
【図１３】並列動作可能性を考慮した場合のＸ、Ｙプロセスの状態遷移図
【図１４】（Ａ）はＸプロセスについての、外部イベントが挿入されたプロセス間通信情報を示す図、（Ｂ）Ｙプロセスについての、外部イベントが挿入されたプロセス間通信情報を示す図
【図１５】（Ａ）はＸプロセスのプロセス間通信情報における応答イベント状態数数を示す図、（Ｂ）はＹプロセスのプロセス間通信情報における応答イベント状態数数を示す図
【図１６】通信プロトコル間に同時起動可能なプロトコルがない場合のシステムについての状態遷移図
【図１７】図１６に示したａプロセスとｂプロセスで構成されるシステムの状態遷移表を示す図
【図１８】通信プロトコル間の一方が同時起動可能なプロトコルがである場合のシステムについての状態遷移図
【図１９】図１８に示したａ’プロセスとｂ’プロセスで構成されるシステムの状態遷移表
【図２０】通信プロトコル間の双方が同時起動可能なプロトコルがである場合のシステムについての状態遷移図
【図２１】図２０に示したａ’’プロセスとｂ’’プロセスで構成されるシステムの状態遷移表を示す図
【図２２】複雑度と、プロセス間関係性、モデル検査意義、モデル検査の有効性との関係を示す表の例を示す図
【図２３】ある状態遷移モデルの状態遷移表の一例を示す図
【図２４】αプロトコルのシーケンス図
【図２５】Ａプロセスの状態遷移表を示す図
【図２６】Ｂプロセスの状態遷移表を示す図
【図２７】βプロトコルのシーケンス図
【図２８】Ａ’プロセスの状態遷移表を示す図
【図２９】Ｂ’プロセスの状態遷移表を示す図
【符号の説明】
【０１００】
１…モデル検査有効性計測装置
２…状態遷移表データ
１０…プロセス間通信情報解析部
２０…プロセス間通信情報格納部
３０…プロセス間通信情報入出力部
４０…並列動作可能入力部
５０…複雑度計算部
６０…複雑度表示部
【図１】
2010262365.tif 000003
【図２】
2010262365.tif 000004
【図３】
2010262365.tif 000005
【図４】
2010262365.tif 000006
【図５】
2010262365.tif 000007
【図６】
2010262365.tif 000008
【図７】
2010262365.tif 000009
【図８】
2010262365.tif 000010
【図９】
2010262365.tif 000011
【図１０】
2010262365.tif 000012
【図１１】
2010262365.tif 000013
【図１２】
2010262365.tif 000014
【図１３】
2010262365.tif 000015
【図１４】
2010262365.tif 000016
【図１５】
2010262365.tif 000017
【図１６】
2010262365.tif 000018
【図１７】
2010262365.tif 000019
【図１８】
2010262365.tif 000020
【図１９】
2010262365.tif 000021
【図２０】
2010262365.tif 000022
【図２１】
2010262365.tif 000023
【図２２】
2010262365.tif 000024
【図２３】
2010262365.tif 000025
【図２４】
2010262365.tif 000026
【図２５】
2010262365.tif 000027
【図２６】
2010262365.tif 000028
【図２７】
2010262365.tif 000029
【図２８】
2010262365.tif 000030
【図２９】
2010262365.tif 000031