図面 (/)

技術 データフローグラフ検証装置

出願人 日本電信電話株式会社
発明者 福田晴元高橋直久
出願日 1993年10月26日 (26年6ヶ月経過) 出願番号 1993-267459
公開日 1995年5月12日 (24年11ヶ月経過) 公開番号 1995-121504
状態 特許登録済
技術分野 データフローマシン
主要キーワード 受け取り状態 判別演算 到達状態 出力アーク 各制御ノード 到着監視 環境レベル 再帰関数
関連する未来課題
重要な関連分野

この項目の情報は公開日時点(1995年5月12日)のものです。
また、この項目は機械的に抽出しているため、正しく解析できていない場合があります

図面 (20)

目的

環境依存発火機能と環境依存分配機能を有するデータフロー計算機で実行される再帰関数を含むプログラムにおいてすべての実行環境ベルについて可到達性異常、伝播異常、全実行性異常、合流異常、関数再帰呼び出しによる再帰異常を検出するデータフローグラフ検証装置を提供する。

構成

再帰関数検証系1および実行経路検証系2を有し、実行経路検証系2の状態演算機能部24はトークンが伝播してきた経路上のノードに着目して、トークンが入力できるかどうかの状態を示す入力状態、ノードが発火するかどうかの状態を示す到達状態、トークンが出力できるかどうかを示す出力状態の各々をすべての入力アークの実行環境レベル毎の状態、入力状態とノードの環境レベル、到達状態と出力アーク先ノードの環境レベルを各々基に実行環境レベル毎に状態演算し、また再帰関数検証系1の有限再帰判別演算機能部15は呼び出し先関数の出力状態を引き継ぎ、関数内のノードを状態演算する。

概要

背景

最初に、本検証装置で対象とするプログラムを実行するデータフロー計算機の動作概要について説明する。

このデータフロー計算機では、数値データ(環境レベルと呼ぶ)を付与したノードからなるデータフローグラフをプログラムとし、数値データ(実行環境ベルと呼ぶ)を付与したトークンを用いる。

ノードの集合をNとする。ノードn(n∈N)の環境レベルをtag(n)と表す。nの第i入力アークの先に接続されたノードの環境レベルをtagin(n,i)、nの第j出力アークの先に接続されたノードの環境レベルをtagout(n,j)と表す。実行環境レベルlを、トークンに付与する。この時、l<tagin(n,i)を満たす環境レベルを持つノードからnへ張られたアークをnの環境入力アークといい、nからl<tagout (n,j)を満たす環境レベルを持つノードへ張られたアークを環境出力アークという。

環境依存発火機能は、全ての環境入力アーク上にトークンが全て揃うまでノードを待機させ、これらのアーク上にトークンが揃った後、ノードを発火させる機能である。環境依存分配機能は、全ての環境出力アーク上に実行環境レベルを与えたトークンを出力する機能である。

以上の機能により、ある実行環境レベルlをトークンに付与してプログラムの実行を開始させると、l以上の環境レベルを持つノード間にだけトークンを伝播させ、l以上の環境レベルを持つノードだけを実行させることができる。

次に、経路識別子を用いた色付きトークンモデルについて説明する。

データフロー実行装置において、色付きトークンの概念を導入することにより、異なる色を持つトークン間で、インタラクションを持たないようにできる。これにより、一つのグラフを複数の色(環境)で同時に実行させることができる。

まず、色付きトークンの基本モデルについて説明する。図2に実行例を示す。図中で「●(K,a)」は、値K色aのトークンを表す。図2(b)では、同じ色を持つトークンが全ての入力アーク上に揃っていないため、ノードの発火は行われない。図2(c)では、同じ色iを持つトークンが全ての入力アーク上に揃ったため、ノードの発火が行われる。このように発火が行われると、データフローグラフを色別に複数の実行環境で共有できる。

検証を行う際に、複数ある経路を全て場合分けし、それらを一つ一つ検証するのでは、分岐命令の数が増えるほどに必要な実行回数が増加する。このため、一つのグラフを一回実行して検証を終了させるために、分岐命令では全ての出力アークに対し、異なる色を与えたトークンを出力する事とする。この際に、図3のような構造をもつプログラムの場合に問題が発生する。図中で太線で示したアーク上には、分岐ノード楕円にSWの文字のあるノード)が新たな色を付与することにより、異なる色を持つトークンが伝播するため発火不可能となる。

上記の問題を解決するために、分岐命令(分岐ノードに与えられる命令)の、分岐経路ごとに、経路断片識別子(直井邦彰、高橋直久:プレスブルガー算術を用いたInteasible Path検出法知能ソフトウェア工学研究会1992,11参照)Idpfを付与する。この系列<Idpf1 ,Idpf2 ,…,Idpfj >を経路識別子と呼ぶ。経路識別子をトークンの色として用いることにより、複数の経路上のトークンを識別できる。制御ノードである分岐ノードでは、入力トークンの色(経路識別子)に対して、分岐方向に応じて異なる経路断片識別子を加えて経路識別子を作成し、これをトークンの色として出力アークに出力する。

ここで、2つの色c1 =<idp11 ,idp12 ,…,Idp1j >,c2 =<idp21 ,idp22 ,…,Idp2k >を考える。このとき、i=1,2,…,j(j<k)において、Idp1i =Idp2i のとき、c1 はc2 の先祖(c2 はc1

概要

環境依存発火機能と環境依存分配機能を有するデータフロー計算機で実行される再帰関数を含むプログラムにおいてすべての実行環境レベルについて可到達性異常、伝播異常、全実行性異常、合流異常、関数再帰呼び出しによる再帰異常を検出するデータフローグラフ検証装置を提供する。

再帰関数検証系1および実行経路検証系2を有し、実行経路検証系2の状態演算機能部24はトークンが伝播してきた経路上のノードに着目して、トークンが入力できるかどうかの状態を示す入力状態、ノードが発火するかどうかの状態を示す到達状態、トークンが出力できるかどうかを示す出力状態の各々をすべての入力アークの実行環境レベル毎の状態、入力状態とノードの環境レベル、到達状態と出力アーク先ノードの環境レベルを各々基に実行環境レベル毎に状態演算し、また再帰関数検証系1の有限再帰判別演算機能部15は呼び出し先関数の出力状態を引き継ぎ、関数内のノードを状態演算する。

目的

本発明は、上記に鑑みてなされたもで、その目的とするところは、環境依存発火機能と環境依存分配機能を有するデータフロー計算機で実行される再帰関数を含むプログラムにおいて全ての実行環境レベルについて可到達性異常と伝播異常と全実行性異常と合流異常と、関数の再帰呼び出しによる再帰異常を検出するデータフローグラフ検証装置を提供することにある。

効果

実績

技術文献被引用数
1件
牽制数
1件

この技術が所属する分野

(分野番号表示ON)※整理標準化データをもとに当社作成

ライセンス契約や譲渡などの可能性がある特許掲載中! 開放特許随時追加・更新中 詳しくはこちら

請求項1

環境レベルを付与したノードアークで結合したデータフローグラフプログラムとし、実行環境ベルを付与したトークンをアークを経由してノード上を伝播させ、環境依存発火機能と環境依存分配機能により発火制御するプログラム内のトークンの伝播上の正常性を検証するデータフローグラフ検証装置であって、トークンが伝播してきた経路上のノードに着目して、トークンが入力できるかどうかの状態を示す入力状態、ノードが発火するかどうかの状態を示す到達状態、トークンが出力できるかどうかを示す出力状態の各々をすべての入力アークの実行環境レベル毎の状態、入力状態とノードの環境レベル、到達状態と出力アーク先ノードの環境レベルを各々基に実行環境レベル毎に状態演算する状態演算機能部と、呼び出し先関数の出力状態を引き継ぎ関数内のノードを状態演算する有限再帰判別演算機能部とを有することを特徴とするデータフローグラフ検証装置。

技術分野

0001

本発明は、環境依存発火機能と環境依存分配機能を有するデータフロー計算機で実行されるプログラムに対するデータフローグラフ検証装置に関する。

背景技術

0002

最初に、本検証装置で対象とするプログラムを実行するデータフロー計算機の動作概要について説明する。

0003

このデータフロー計算機では、数値データ(環境レベルと呼ぶ)を付与したノードからなるデータフローグラフをプログラムとし、数値データ(実行環境ベルと呼ぶ)を付与したトークンを用いる。

0004

ノードの集合をNとする。ノードn(n∈N)の環境レベルをtag(n)と表す。nの第i入力アークの先に接続されたノードの環境レベルをtagin(n,i)、nの第j出力アークの先に接続されたノードの環境レベルをtagout(n,j)と表す。実行環境レベルlを、トークンに付与する。この時、l<tagin(n,i)を満たす環境レベルを持つノードからnへ張られたアークをnの環境入力アークといい、nからl<tagout (n,j)を満たす環境レベルを持つノードへ張られたアークを環境出力アークという。

0005

環境依存発火機能は、全ての環境入力アーク上にトークンが全て揃うまでノードを待機させ、これらのアーク上にトークンが揃った後、ノードを発火させる機能である。環境依存分配機能は、全ての環境出力アーク上に実行環境レベルを与えたトークンを出力する機能である。

0006

以上の機能により、ある実行環境レベルlをトークンに付与してプログラムの実行を開始させると、l以上の環境レベルを持つノード間にだけトークンを伝播させ、l以上の環境レベルを持つノードだけを実行させることができる。

0007

次に、経路識別子を用いた色付きトークンモデルについて説明する。

0008

データフロー実行装置において、色付きトークンの概念を導入することにより、異なる色を持つトークン間で、インタラクションを持たないようにできる。これにより、一つのグラフを複数の色(環境)で同時に実行させることができる。

0009

まず、色付きトークンの基本モデルについて説明する。図2に実行例を示す。図中で「●(K,a)」は、値K色aのトークンを表す。図2(b)では、同じ色を持つトークンが全ての入力アーク上に揃っていないため、ノードの発火は行われない。図2(c)では、同じ色iを持つトークンが全ての入力アーク上に揃ったため、ノードの発火が行われる。このように発火が行われると、データフローグラフを色別に複数の実行環境で共有できる。

0010

検証を行う際に、複数ある経路を全て場合分けし、それらを一つ一つ検証するのでは、分岐命令の数が増えるほどに必要な実行回数が増加する。このため、一つのグラフを一回実行して検証を終了させるために、分岐命令では全ての出力アークに対し、異なる色を与えたトークンを出力する事とする。この際に、図3のような構造をもつプログラムの場合に問題が発生する。図中で太線で示したアーク上には、分岐ノード楕円にSWの文字のあるノード)が新たな色を付与することにより、異なる色を持つトークンが伝播するため発火不可能となる。

0011

上記の問題を解決するために、分岐命令(分岐ノードに与えられる命令)の、分岐経路ごとに、経路断片識別子(直井邦彰、高橋直久:プレスブルガー算術を用いたInteasible Path検出法知能ソフトウェア工学研究会1992,11参照)Idpfを付与する。この系列<Idpf1 ,Idpf2 ,…,Idpfj >を経路識別子と呼ぶ。経路識別子をトークンの色として用いることにより、複数の経路上のトークンを識別できる。制御ノードである分岐ノードでは、入力トークンの色(経路識別子)に対して、分岐方向に応じて異なる経路断片識別子を加えて経路識別子を作成し、これをトークンの色として出力アークに出力する。

0012

ここで、2つの色c1 =<idp11 ,idp12 ,…,Idp1j >,c2 =<idp21 ,idp22 ,…,Idp2k >を考える。このとき、i=1,2,…,j(j<k)において、Idp1i =Idp2i のとき、c1 はc2 の先祖(c2 はc1

0013

次に、データフローグラフの検証方式について説明する。

0014

まず、扱う構造について説明する。本検証装置により検出される、可到達性異常、伝播異常、全実行性異常、合流異常のいずれでもないプログラムは「良構造」であるという。以下の構造をもつプログラムは通常の実行時には正しく実行されるが、本検証法では合流異常として判定される。これらの構造は同じ機能をもつ良構造へ変換可能であるため問題はない。

0015

図4(a)に示す分岐ノードを用いてサイクルを構成する繰り返し構造を考える。この構造は図4(b)に変更可能である。このような指定繰り返し構造は関数再起呼び出しに変換可能であるため、本検証系では、サイクルを構成しないプログラムだけを許し、図4(a)のようなサイクルを含む構造は合流異常があると判定する。

0016

また、図5(a)に示す複数の経路が一つの実行経路を共有する構造は実行時にエラーを発生しない。しかし、この構造は図中の(b)に示すような、より簡明な構造に変換可能である。このため、本検証系では、図5(c)に例示するように、分岐ノードと合流ノードの対により分岐構造ネストしてできるプログラム構造だけを許し、図5(a)のようなネストしない構造は合流異常があると判定する。

0017

次に、検出する異常について説明する。図1に異常があるプログラムの例を示す。図1において、白丸のノードは演算ノード黒丸のノードは分配ノード、白丸にSのノードは開始ノード、白丸にEのノードは終了ノード、白丸にSWのノードは分岐ノード、逆三角形のノードは合流ノード、四角のノードは上述のノードにより形成される一つの経路を表す。また、ノードの左上の数字ノード番号を示す。以下に各異常について述べる。

0018

まず、伝播異常は、開始ノードからトークンを出力しない終了ノード以外のノードに至る経路が存在するとき、伝播異常であるという。図1(g)のノード4においては出力アークが存在しないためトークンを出力できない。

0019

可到達性異常は、開始ノードから終了ノードまでトークンが伝播する経路が存在しないとき、可到達性異常であるという。例えば図1において、(a)のノード2、(d)のノード6においてはトークンを出力できないため、また、(b)のノード4、(c)のノード3においては入力アーク上にトークンが揃わないため実行が停止し、終了ノードへトークンが到達しない。

0020

全実行性異常は、開始ノードからトークンが到達する経路がないノードが存在するとき、全実行性異常であるという。例えば図1において、(b)のノード2、(c)のノード2は入力アークが存在しないため、発火する可能性はない。

0021

合流異常は、分岐命令により分岐した経路をまとめること以外の目的で使用する合流ノードが存在する合流異常であるという。例えば図1において、(e)のノード5では、合流ノードより先の経路を2つのトークンが伝播し、衝突することとなる。図1において、(f)のノード2〜4の間は常にループ状態となり、先の経路上でトークンが衝突することとなる。

0022

前述の経路断片識別子を値として持つトークンを検証実行に用いることにより、プログラムが良構造であるかを検出する。このために、発火規則を以下のように定める。

0023

合流ノードの場合は、例えば、図6のような経路断片識別子の割り当てを表す木が与えられた場合には、値としてc1 とc2 もしくは、c3 とc4 のよう兄弟関係にある経路断片識別子をもつトークンどうしが入力アーク上に揃った場合に発火する。

0024

その他としては、等しい経路断片識別子をもつトークンが入力アーク上に揃った場合に発火する。

0025

次に、検証のための実行法について説明する。ノードの実行状態を示すことにより、全実行性異常を検出する。このために、各ノードに対してフラグを付与する。このフラグを実行フラグと呼ぶ。実行フラグの値が1のときは、そのノードが実行されることを、0のときは実行されないことを表す。初期値は0である。

0026

本検証装置は、データフローグラフ上の全てのノードに対して付与した実行フラグを0に初期化した後、以下に示す方式で処理を施す。
1.全ての入力アーク上にトークンが到達するまで待機させる。
2.入力アーク上にトークンが揃った後、前節で述べた発火規則に添ってノードの発火を行う。このとき、ノードの実行フラグを1にし、入力アーク上のトークンをノード内に取り込む。
3.ノード内のトークンの値をコピー(合流ノードの場合はトークンの値を親となる経路断片識別子を値とする)したトークンを出力アーク上に出力する。出力アークが存在しない場合は、トークンをノード内に取り込んだままとする。

0027

それぞれのノードを上記の実行方式に従って発火させることにより、グラフ全体を非同期並列に実行する。

0028

異常の検出条件について説明する。本検証装置により、検証対象とするプログラムを実行させ、実行中のノードがなくなった時点で検証のための実行を終了する。この際に、次の表1に示すことが言える。

0029

ID=000004HE=110 WI=159 LX=0255 LY=0450
図7は、従来の検証装置の構成を示す。図中で、実線矢印は制御の流れを、点線矢印はデータの流れを表す。図中の各機能について説明する。
トークン到着監視機能:全ての入力アーク上にトークンが揃ったノードを検出し、発火規則を基に発火させる。ノードが発火した場合は、ノードの実行フラグを1にして制御をトークン入力機能に移す。
トークン入力機能:入力アーク上のトークンを、入力アークの順に並べてノード内に取り込む。
ノード分類機能:発火したノードを演算命令分配命令、分岐命令、手続き呼び出し命令、手続開始命令、手続き復帰命令、合流命令に分類し、そのノード種別トークン出力機能に送る。
トークン出力機能A:トークン出力機能Aの詳細構成図を図8に示す。図中で、実線矢印は制御の流れを、点線矢印はデータの流れを表す。命令デコード機構は、lineAに流れてきたデータよりノード種別を知り、対応する出力機構へ制御を移行する。トークン消去機構はノード内に取り込んだトークンを消去する。各出力機構は命令の種類に応じて以下の様に動作する。なお、入力アーク上に到達したトークンとは、ノード内に取り込んだトークンのことを指す。

0030

演算命令出力機構は、入力アーク上に到達したトークンの値をコピーしてトークンを生成し、出力アーク上に置く。

0031

分配命令出力機構は、入力アーク上に到達したトークンの値をコピーして新たにトークンを生成し、全ての出力アーク上へ置く。

0032

分岐命令出力機構は、第2入力アーク上に到達したトークンの値より得られる経路断片識別子の孫値を2つ求める。求めた2つの経路断片識別子を値とする2つのトークンを生成し、それぞれ出力アーク上へ置く。

0033

手続き呼び出し命令出力機構は、第2入力アーク上のトークンをコピーし、手続き開始ノードの第1入力アーク上に置く。また、出力アークの名前を値としたトークンを生成する。第1入力アーク上のトークンの値として格納されている関数名から関数の手続き復帰ノードを求め、そのノードの第1入力アーク上に、生成したトークンを置く。

0034

手続き開始命令出力機構は、入力アーク上のトークンのコピーを出力アーク上に置く。

0035

手続き復帰命令出力機構は、第2入力アーク上の値を使用してトークン(結果の値)を生成する。第1入力アーク上のトークンの値として指定されたアークにトークン(戻り先)を置く。

0036

合流命令出力機構は、各入力アーク上のトークンの値より得られる経路断片識別子に対し、共通の先祖となる値を求める。求めた経路断片識別子を値とするトークンを生成し、このトークンを出力アーク上へ置く。

0037

図9に実行例を示す。図中で黒丸はトークン、白丸ノードは演算ノード、白丸に十字のノードは分配ノードを表す。また、斜線ノードは実行フラグの立ったノードを表す。以下に実行例の動作説明を示す。
1.開始ノードより経路断片識別子c1 なる値を持つトークンを出力する。関数呼び出しノードでは、値がc1 であるトークンを手続き開始ノードの入力アーク上へ置く(図9(c))。
2.関数の検証が終了し、手続き復帰ノードが発火した場合には、手続き復帰ノードの第1入力アークに置かれたトークンの値より復帰先アークを求め、求めたアーク上にトークンを置く(図9(d))。
3.分岐ノードでは入力アーク上のトークンの値より得られる経路断片識別子

0038

図9のように、全ての入力アーク上にトークンが揃った場合に、ノードに実行フラグを立てて、出力アーク上にトークンを置く。トークンが終了ノードに至った後(図9(f)の時)、グラフ上に表1の検出条件を持つトークンやノードは存在しないため、異常のないプログラムと言える。

発明が解決しようとする課題

0039

環境依存発火機能・環境依存分配機能を有するデータフロー計算機で実行されるプログラムに従来の検証装置を適用した場合、異常が検出されなくとも、ノードへの環境レベルの付け方によっては、ある実行環境レベルでは、可到達性異常、伝播異常、全実行性異常、合流異常が生じる場合がある。

0040

例えば、図10のように環境レベルを配したプログラムを考える。ここで、白丸のノードは演算ノードを表し、白丸に十字のノードは分配ノードを表す。各ノードの左側の数値はノード番号を表し、右側の数値は環境レベルを表す。実行環境レベル1,2のトークンを用いた場合には、図10(a),(b),(c)のどのプログラムにおいても正常に動作する。しかし、実行環境レベル3のトークンが伝播する場合には、図10(a)〜(c)の各プログラムでそれぞれ以下に示す問題が発生する。

0041

図10(a)では、ノード1からノード10まで、実行環境レベル3のトークンが伝播する経路がある。しかし、ノード6は環境レベルが3であるにもかかわらず、実行環境レベル3のトークンは到着しないため、実行は行われない。

0042

図10(b)では、ノード1からノード10まで、実行環境レベル3のトークンが伝播する経路は存在する。しかし、ノード4に到達した実行環境レベル3のトークンは、これより先のノードを実行できない。このため、このトークンはノード10に到達しない。

0043

図10(c)では、ノード7に到達した実行環境レベル3のトークンは、これより先のノードを実行できない。このため、トークンはノード10に到達しない。

0044

実行環境レベル別に実行を行った場合には、上述した誤りが発生する可能性がある。しかし、従来の検証装置による検証では、グラフの構造による可到達性異常と伝播異常と全実行性異常と合流異常を検出するだけであり、任意の環境レベルに対する可到達性異常と伝播異常と全実行性異常と合流異常の検出は行っていない。このため上述の誤りを検出できない。

0045

また図11にあるように、自関数の再帰呼び出しにより停止しない構造が考えられるが、従来の検証法ではこのような構造を検出できず、また、検証のための実行が停止しない。この異常を再帰異常と呼ぶ。

0046

この問題を解決するために、与えられた実行環境レベルで実行されるべきノードが全て実行され、かつ、プログラムの開始ノードから終了ノードまでトークンが伝播することを、全ての実行環境レベルにおいて検出する必要がある。

0047

本発明は、上記に鑑みてなされたもで、その目的とするところは、環境依存発火機能と環境依存分配機能を有するデータフロー計算機で実行される再帰関数を含むプログラムにおいて全ての実行環境レベルについて可到達性異常と伝播異常と全実行性異常と合流異常と、関数の再帰呼び出しによる再帰異常を検出するデータフローグラフ検証装置を提供することにある。

課題を解決するための手段

0048

上記目的を達成するため、本発明のデータフローグラフ検証装置は、環境レベルを付与したノードをアークで結合したデータフローグラフをプログラムとし、実行環境レベルを付与したトークンをアークを経由してノード上を伝播させ、環境依存発火機能と環境依存分配機能により発火制御するプログラム内のトークンの伝播上の正常性を検証するデータフローグラフ検証装置であって、トークンが伝播してきた経路上のノードに着目して、トークンが入力できるかどうかの状態を示す入力状態、ノードが発火するかどうかの状態を示す到達状態、トークンが出力できるかどうかを示す出力状態の各々をすべての入力アークの実行環境レベル毎の状態、入力状態とノードの環境レベル、到達状態と出力アーク先ノードの環境レベルを各々基に実行環境レベル毎に状態演算する状態演算機能部と、呼び出し先関数の出力状態を引き継ぎ、関数内のノードを状態演算する有限再帰判別演算機能部とを有することを要旨とする。

0049

本発明のデータフローグラフ検証装置では、トークンが伝播してきた経路上のノードに着目して、入力状態、到達状態、出力状態の各々をすべての入力アークの実行環境レベル毎の状態、入力状態とノードの環境レベル、到達状態と出力アーク先ノードの環境レベルの各々に基づいて実行環境レベル毎に状態演算し、呼び出し先関数の出力状態を引き継ぎ、関数内のノードを状態演算する。

0050

以下、図面を用いて本発明の実施例を説明する。

0051

なお、実施例を説明する前に、まず本発明のデータフローグラフ検証装置の基本概念について説明する。本検証装置は、任意の環境レベルに対する可到達性異常、伝播異常、全実行性異常、合流異常、再帰異常を検出するための手段1、および関数の再帰呼び出しによる停止しない状態を検出するための手段2を有する。

0052

まず、手段1について説明し、その中の状態演算について説明する。

0053

実行環境レベルは数値(ここでは自然数を用いる)で表す。数値が大きいほどレベルが高いことを意味する。ここで、ある実行環境レベルにおけるトークン伝播の状況を、その実行環境レベルの状態といい、その値を次の様に表す。
T:通常のプログラム実行時にトークンが伝播してくる可能性がある。
N:通常のプログラム実行時にトークンは伝播してこない。
R:通常のプログラム実行時に、発火出来ない。もしくは、トークンを出力出来ない状態が発生している。
E:通常のプログラム実行時に実行されない状態が発生している。

0054

ID=000006HE=010 WI=124 LX=0430 LY=1200
s2 なる演算を次の様に定義する。

0055

ID=000007HE=140 WI=124 LX=0430 LY=1400
また、レベルlの実行環境レベルの状態を第l要素とした、全ての実行環境レベルの状態を表す一次元ベクトル状態ベクトルと呼ぶ。このとき状態ベクトルS1 =(s11,s12,…,s1n),S2 =(s21,s22,…,s2n)に対して、

0056

ID=000010HE=030 WI=124 LX=0430 LY=1200
入力状態ベクトルをI=(i1 ,i2 ,…,im ,…,in )としたとき、各要素が、次式により求まる。

0057

R=(r1 ,r2 ,…,rm ,…,rn )を到達状態ベクトル、到達状態ベクトルを求める演算を、到達状態演算と呼ぶ。到達状態ベクトルの第m要素の値がTのとき、実行環境レベルmのトークンで、ノードが発火することを示す。なお、tagはノードの環境レベルである。

0058

ID=000011HE=030 WI=124 LX=0430 LY=1750
到達状態ベクトルをR=(r1 ,r2 ,…,rm ,…,rn )としたとき、第j出力アークに対し、各要素が次式により求まるOj =(oj1,oj2,…,ojm,…,ojn)を出力状態ベクトル、出力状態ベクトルを求める演算を、出力状態演算と呼ぶ。出力状態ベクトルの第m要素の値がTのとき、実行環境レベルmのトークンを出力できることを示す。なお、tagout (j)は第j出力アーク先

0059

ID=000013HE=055 WI=124 LX=0430 LY=0300
図12に示す状態演算機能により、各実行環境レベルにおける可到達性異常、伝播異常、全実行性異常、合流異常、再帰異常を検出する。図中で実線矢印は制御の流れ、点線矢印はデータの流れを表す。データフローグラフの各ノードに対してRフラグ、Eフラグと呼ぶ二つの一次元ベクトルを持たせる。これらのフラグの第m要素は、実行環境レベルmでの異常発生状況を表す。Rフラグの要素の値が1の時、その要素に対応する実行環境レベルで、そのノードが発火出来ないか、トークンを出力できないことを意味する。Eフラグの要素の値が1の時、その要素に対応する実行環境レベルでそのノードの入力アーク上にトークンが到達しないため、そのノードが実行されないことを意味する。

0060

これらのフラグの要素の初期値は、0である。以下に、状態演算機能の各機構について述べる。

0061

読み取り機構は、ノード内に取り込まれたトークンより値を読み取り、その値をデータとして入力状態演算機構へ送る。

0062

出力アーク判定機構は、出力アーク先にあるノードの環境レベルをデータとして、出力状態演算機構へ送る。

0063

入力状態演算機構は、値読み取り機構よりトークンの値を受け取り、また、lineAよりノード種別を受け取り、入力状態演算を行う。演算結果をデータとして到達状態演算機構に送る。入力トークンの値にRが含まれず、式(7)の結果にRとなる要素がある場合には、その要素に対応するRフラグの値を1とする。

0064

到達状態演算機構は、入力状態演算機構より入力状態演算の結果を受け取り、到達状態演算を行う。演算結果をデータとして出力状態演算機構に送る。入力状態演算機構より受け取った値の要素がEもしくはNであり、演算によりRが得られた要素がある場合には、その要素に対応するRフラグの値を1とする。また、入力状態演算機構より受け取った値の要素がNまたはEであり、演算によりEが得られた要素がある場合には、その要素に対応するEフラグの値を1とする。

0065

出力状態演算機構は、到達状態演算機構より到達状態演算の結果を受け取り、lineAよりノード種別を受け取り、また、出力アーク判定機構より出力アーク先にあるノードの環境レベルを受け取り出力状態演算を行う。演算結果をデータとして出力する。演算によりRが得られた要素がある場合には、その要素に対応するRフラグの値を1とする。

0066

状態演算機能を有する実行経路検証系では、データフローグラフの全てのノードに対して以下に示す方式で処理を施すことにより検証のための実行を行う。

0067

1.全ての入力アーク上にトークンが到達するまで待機させる。
2.入力アーク上にトークンが揃った後、従来技術と同じ発火規則に添ってノ
ードの発火を行う。このとき、ノードの実行フラグを1にし、入力アーク上のトークンをノード内に取り込む。
3.状態演算機能は各機構を動作させる。
4.出力状態演算機構からの出力と、ノード内に取り込んだトークンの経路断片識別子と有限再帰判別ベクトルより新たにトークンを生成する。新たに生成したトークンを出力アーク上に出力する。ノード内のトークンを消去する。

0068

次に、手段2について説明する。

0069

有限再帰判別ベクトルは、関数の相互呼び出しによる実行停止性を表す論理値を要素として持つ一次元ベクトルであり、要素の値が1のとき呼び出しが停止することを表し、0のとき停止しないことを表す。なお、プログラムが使用している関数名とこの有限再帰判別ベクトルと実行経路検証系より得られた関数の状態ベクトルを対応付ける表を関数表と呼ぶ。

0070

実行経路検証系で検証を行い、ノードが発火した際に、各ノードごとに以下に示す有限再帰判別演算を行う。

0071

合流ノードに対しては、各トークンの値より得た有限再帰判別ベクトルの各要素について論理和を求める。

0072

手続き呼び出しノードに対しては、各トークンの値として与えた有限再帰判別ベクトルの各要素について論理積を求める。さらに求めた有限再帰判別ベクトルと関数用の呼び出し先関数の有限再帰判別ベクトルの各要素について論理積を求める。

0073

その他のノードに対しては、各要素について論理積を求める。

0074

再帰関数検証系では、実行経路検証系が検証のための実行を行う際に以下のように動作する。
1.プログラムで使用している関数の中で検証を行う関数を求め、その検証対象関数名と検証対象関数の有限再帰判別ベクトルと全ての要素がTの状態ベクトルを実行経路検証系に送る。
2.実行経路検証系の状態演算機能の実行後に、有限再帰判別演算を行う。
3.実行経路検証系より関数に対する検証のための実行が終了した信号を受け取った際には、検証を行った関数の状態を調べ、関数表の中でその関数の項を更新する。プログラムに対する検証のための実行の終了判定を行い、終了しない場合は1に戻る。

0075

上述したように、状態演算機能を有するデータ駆動実行型検証装置により、検証のための実行を行い、実行中のノードがなくなった時点で、もしくは終了判定機能により終了することを決定した時点で検証のための実行を終了する。このとき、トークンの位置と値、およびノードのフラグの値を調べることにより可到達異常、伝播異常、全実行異常、合流異常を知ることができ、また有限再帰判別ベクトルの値を調べることにより、関数の相互再帰呼び出しによる再帰異常を知ることができる。

0076

次に、本発明の実施例について詳細に説明する。

0077

なお、本実施例では、発火規則は次のように定める。関数復帰ノードでは、第2入力アーク上にトークンが到達した際に発火する。他のノードは従来技術と同様である。

0078

図13は、状態演算機能を有する本実施例の検証装置の構成を示すブロック図である。図13において、実線の矢印は制御の流れを表し、点線の矢印はデータの流れを表す。

0079

図13に示す本検証装置は、再帰関数検証系1および実行経路検証系2を有する。再帰関数検証系1は、関数表作成機能部11、検証関数更新機能部12、関数表更新機能部13、終了判定機能部14、有限再帰判別演算機能部15から構成されている。実行経路検証系2は、色付きトークン到達監視機能部21、トークン入力機能部22、ノード分類機能部23、状態演算機能部24、トークン出力機能B部25、関数実行終了判定機能部26から構成されている。

0080

まず、再帰関数検証系1の各構成要素について説明する。

0081

関数表作成機能部11は、検証対象プログラムで使用する関数名と全ての要素の値が0の有限再帰判別ベクトルと全ての要素がNである状態ベクトルとの対応を表す関数表を作成する。作成した関数表を記憶装置内の関数表および既関数表として登録する。また、記憶装置内の検証関数名を空にする。最後に検証関数更新機能部12に制御を移行する。

0082

検証関数更新機能部12は、記憶装置より関数表と検証関数名を得る。次に検証関数名よりまだ検証していない関数を求め、その関数の全てのノードの実行フラグ、Rフラグ、Eフラグを初期化し、トークンを消去する。関数の開始ノード(もしくは、手続き開始ノードの入力アーク上)に対して、ノードに与えられた環境レベルのなかで最大の値と対応する要素までをTとし、それ以上をNとした状態ベクトルと要素の値が1の有限再帰判別ベクトル、そして経路断片識別子を値とするトークンを置き、関数名を検証関数名に登録する。全ての関数に対する検証が終了した場合は終了判定機能部14に制御を移行する。

0083

関数表更新機能部13は、終了ノードにトークンが存在する関数について、そのトークンの値から得られる有限再帰判別ベクトルの値と状態ベクトルを、記憶装置内関数表の対応する関数の有限再帰判別ベクトルと状態ベクトルに代入する。検証関数更新機能部12に制御を移行する。

0084

終了判定機能部14は、記憶装置内の関数表と既関数表とを比較し、等しい場合は検証のための実行を終了する。異なる場合は、記憶装置内の関数表を既関数表として記憶装置に登録し、記憶装置内の検証関数名を空にする。制御を検証関数更新機能部12に移行する。

0085

有限再帰判別演算機能部15は、状態演算機能よりノード種別を受け取り有限再帰判別演算を行う。演算結果とノード種別をトークン出力機構に送り、制御をトークン出力機能B部25に移す。

0086

次に、実行経路検証系2の各構成要素について説明する。

0087

トークン到達監視機能部21、トークン入力機能部22、ノード分類機能部23は従来技術のものと同じであり、次の通りである。

0088

トークン到達監視機能部21は、全ての入力アーク上にトークンが揃ったノードを検出し、発火規則を基に発火させる。ノードが発火した場合は、ノードの実行フラグを1にして制御をトークン入力機能に移す。

0089

トークン入力機能部22は、入力アーク上のトークンを、入力アークの順に並べてノード内に取り込む。

0090

ノード分類機能部23は、発火したノードを演算命令、分配命令、分岐命令、手続き呼び出し命令、手続き開始命令、手続き復帰命令、合流命令に分類し、そのノード種別をトークン出力機能に送る。

0091

状態演算機能部24は、ノード分類機能部23よりノード種別を受け取り状態演算を行う。演算結果とノード種別を有限再帰判別演算機能部15に送り、制御を有限再帰判別演算機能部15に移す。

0092

トークン出力機能B部25の詳細構成図を図14に示す。図中で、実線矢印は制御の流れを、点線矢印はデータの流れを表す。命令デコード機構は、lineBに流れてきたデータにより、ノード種別を知る。次に、対応する出力機構に対して、lineAに流れてきた状態ベクトルと、lineCに流れてきた有限再帰判別ベクトルをデータとして対応する出力機構に送り、制御を移行する。トークン消去機構はノード内に取り込んだトークンを消去する。各出力機構は命令の種類に応じて以下の様に動作する。以降トークンとはノード内に取り込んだトークンのことを指す。

0093

演算命令出力機構は、入力アーク上に到達したトークンの値の経路断片識別子と、命令デコード機構より受け取ったデータを値としてトークンを生成し、出力アーク上に置く。

0094

分配命令出力機構は、トークンの値の経路断片識別子と命令デコード機構より受け取ったデータを値とするトークンを生成し、全ての出力アーク上へ置く。

0095

分岐命令出力機構は、第2入力アークに到達したトークンの値の経路断片識別子に対する孫値を2つ求める。求めた2つの経路断片識別子と命令デコード機構より受け取ったデータを値とする2つのトークンを生成する。新たに生成したトークンをそれぞれの出力アーク上へ置く。

0096

手続き呼び出し命令出力機構は、命令デコード機構より受け取ったデータの有限再帰判別ベクトルと、関数表より求めた呼び出し先関数の有限再帰判別ベクトルと、各要素ごとに論理積を求める。命令デコード機構より受け取ったデータの状態ベクトルと、呼び出し先関数の状態ベクトルを関数表より求めて、式(5)により新たな状態ベクトルを求める。命令デコード機構より受け取った状態ベクトルの要素にRが含まれず、演算結果にRの要素がある場合には、その要素に対応するRフラグの値を1とする。最終的に得られた有限再帰判別ベクトルと状態ベクトル、第2入力アーク上に到達したトークンの値の経路断片識別子を値とするトークンを生成する。生成したトークンを出力アーク上に置く。

0097

手続き開始命令出力機構は、トークンの値の経路断片識別子と命令デコード機構より受け取ったデータを値とするトークンを生成し、出力アーク上へ置く。

0098

手続き復帰命令出力機構は、動作しない。

0099

合流命令出力機構は、各トークンの値より得られる経路断片識別子に対し、共通の先祖となる値を求める。求めた経路断片識別子と命令デコード機構より受け取ったデータを値とするトークンを生成し、このトークンを出力アーク上へ置く。

0100

関数実行終了判定機能部26は、検証実行中の関数の終了ノードのみにトークンがある場合、関数表更新機能部13に制御を移行する。それ以外の場合には色付きトークン到達監視機能部21へ制御を移行する。

0101

次に、演算命令、分配命令、分岐命令、手続き呼び出し命令、合流命令の実行例を示す。以降で用いる図では、点線の白丸ノードは演算ノードもしくは各制御ノード、「●((…),a,b)」は状態ベクトル(…)と経路断片識別子aと有限再帰判別ベクトルbを値として持つトークン、右下側のベクトルは、Rフラグ、左下側のベクトルはEフラグを表す。ノードの環境レベルを右上に示す。

0102

図15に演算命令の処理例を示す。図中で白丸は演算ノードを表す。演算命令では以下のような処理を行う。
(1)トークンが、演算ノードの全ての入力アーク上に揃い、発火規則にも合致するため、演算ノードは発火する。
(2)入力状態演算、到達状態演算、出力状態演算を行う。出力状態演算で求めた到達状態ベクトルの第4要素がRとなったので、Rフラグの第4要素の値を1にする。
(3)ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル(11111)と出力状態ベクトルと経路断片識別子c1 を値とするトークンを出力アーク上に置く。

0103

図16に分配命令の実行例を示す。図中で白丸に十字のノードは分配ノードを示す。分配命令では以下のような処理を行う。
(1)トークンが分配ノードの入力アーク上に到達し、発火規則にも合致するため、分配ノードは発火する。
(2)入力状態演算、到達状態演算、出力状態演算を行う。出力状態演算で求めた出力状態ベクトルの第4要素がRとなったので、Rフラグの第4要素の値を1とする。
(3)ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル(11111)と出力状態ベクトルと経路断片識別子c1 を値とするトークンを出力アーク上に置く。

0104

図17に分岐命令の処理例を示す。図中で楕円型のノードは分岐ノードを示す。分岐命令では以下のように処理を行う。
(1)トークンが分岐ノードの入力アーク上に到達し、発火規則にも合致するため、分岐ノードは発火を行う。
(2)入力状態演算、到達状態演算、出力状態演算を行う。到達状態演算で求めた到達状態ベクトルの第5要素がEとなったので、Eフラグの第5要素の値を1にする。また、出力状態演算の際に、求めた出力状態レベルの第3、第4要素がRと求まったので、Rフラグの第3、第4要素の値を1にする。
(3)ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。経路断片識別子c1 の孫値となる値(c11,c12)を求める。図の場合には、真側の出力アーク上に真側の出力状態ベクトルと有限再帰判別ベクトル(11111)と経路断片識別子c11を、側の出力アーク上に偽側の出力状態ベクトルと有限再帰判別ベクトル(11111)と経路断片識別子c12を値とするトークンを置く。

0105

図18に手続き呼び出し命令の処理例を示す。図中で長方形型のノードは手続き呼び出しノードを示す。手続き呼び出し命令では以下のように処理を行う。
(1)トークンが手続き呼び出しノードの入力アーク上に到達し、発火規則にも合致するため、手続き呼び出しノードは発火する。
(2)入力状態演算、到達状態演算、出力状態演算を行う。入力状態演算で求めた入力状態ベクトルの第4要素が新たにRとなったので、Rフラグの第4要素の値を1にする。求めた状態ベクトルと関数表より得た状態ベクトルとを式(5)で演算を行い、状態ベクトルを求める。
(3)ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル(00111)と経路断片識別子c1 と出力状態ベクトルを値とするトークンを出力アーク上に置く。

0106

図19に合流命令の処理例を示す。図中で逆三角形のノードは合流ノードを示す。合流命令では以下のように処理を行う。
(1)トークンがノード3の入力アーク上に到達し、発火規則にも合致するため、ノード3は発火を行う。
(2)ノード3において、入力状態演算、到達状態演算、出力状態演算を行う。
(3)ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル(11111)と経路断片識別子c1 と出力状態ベクトルを値とするトークンを出力アーク上に置く。

0107

図20に実行例を示す。図中で白丸ノードは演算ノード、楕円のノードは分岐ノード、白丸に十字のノードは分配ノード、長方形のノードは関数呼び出しノードを表す。網掛けのノードは実行フラグの立ったノード、ノードの右上の数字は環境レベル、左下のベクトルはEフラグを、右下のベクトルはRフラグを表す(図では更新されたフラグのみ記す)。ノードに与えられた環境レベルの中で、最大となるものは3であるため、全ての要素が”T”である3要素の状態ベクトルと、”c”なる経路断片識別子と全ての要素の値が1の有限再帰判別ベクトルを値として持つトークンを、開始ノードにおいて処理を始める。

0108

1.図20(1)の関数呼び出しノードが発火する際に、入力アーク上には((TTN),c,(111))なる値を持つトークンが伝播してくる。発火した後には、出力状態ベクトルは(TTN)と求まる。関数表の呼び出し先関数fの項の状態ベクトル(NNN)と求めた出力状態ベクトルとで式(5)の演算を行うと(RRN)が求まる。新たに第1,2要素がRと求まったのでRベクトルの第1,2要素を1にする。また、入力トークンの有限再帰判別ベクトルの論理積により(111)が求まる。この有限再帰判別ベクトルと関数表の有限再帰判別ベクトルとの論理積により(000)が求まる。従って、関数呼び出し命令の出力アーク上に((RRN),c,(000))なる値を持つトークンを出力する(図20(1))。
2.図20(2)の分岐ノードが発火する際に、入力アーク上にはそれぞれ((RRT),c,(000)),((RRN),c,(000))なる値を持つトークンが伝播してくる。発火した後には出力状態ベクトルは(RRR)と求まる。新たに第3要素がRと求まったのでRベクトルの第3要素を1にする。有限

0109

発明の効果

0110

以上説明したように、本発明によれば、状態演算機能を有するデータ駆動実行型検証装置により検証のための実行を行い、実行中のノードがなくなった時点で、または終了判定機能により終了することを決定した時点で検証のための実行を終了し、この時トークンの位置と値、およびノードのフラグの値を調べることにより可到達異常、伝播異常、全実行異常、合流異常を検出することができ、また有限再帰判別ベクトルの値を調べることにより関数の相互再帰呼び出しによる再帰異常を検出することができる。

図面の簡単な説明

0111

図1異常のあるプログラムの例および検出できる異常の例を示す図である。
図2色付きトークンによる実行例を示す図である。
図3分岐ノードで色を与える際の問題点を示す説明図である。
図4扱う構造(繰り返しの表現)を示す図である。
図5扱う構造(分岐と合流)を示す図である。
図6経路断片識別子の例を示す図である。
図7従来の色付きトークンによるデータ駆動実行型検証装置の構成を示すブロック図である。
図8図7の検証装置に使用されているトークン出力機能Aの詳細な構成を示すブロック図である。
図9従来のデータ駆動実行による検証例を示す図である。
図10不完全な実行を行うグラフの例を示す図である。
図11自関数の再帰呼出状態を示す図である。
図12状態演算機能を示す図である。
図13本発明の一実施例に係わる状態演算機能を有する検証装置の構成を示すブロック図である。
図14図13の検証装置に使用されているトークン出力機能B部の構成を示すブロック図である。
図15演算命令の処理例を示す図である。
図16分配命令の処理例を示す図である。
図17分岐命令の処理例を示す図である。
図18手続き呼び出し命令の処理例を示す図である。
図19合流命令の処理例を示す図である。
図20状態演算機能を用いた検証例を示す図である。

--

0112

1再帰関数検証系
2実行経路検証系
11関数表作成機能部
12検証関数更新機能部
13 関数表更新機能部
14終了判定機能部
15有限再帰判別演算機能部
21色付きトークン到達監視機能部
22 トークン入力機能部
23ノード分類機能部
24状態演算機能部
25トークン出力機能B部
26関数実行終了判定機能部

ページトップへ

この技術を出願した法人

この技術を発明した人物

ページトップへ

関連する挑戦したい社会課題

該当するデータがありません

関連する公募課題

該当するデータがありません

ページトップへ

技術視点だけで見ていませんか?

この技術の活用可能性がある分野

分野別動向を把握したい方- 事業化視点で見る -

(分野番号表示ON)※整理標準化データをもとに当社作成

ページトップへ

おススメ サービス

おススメ astavisionコンテンツ

新着 最近 公開された関連が強い技術

この 技術と関連性が強い技術

関連性が強い 技術一覧

この 技術と関連性が強い人物

関連性が強い人物一覧

この 技術と関連する社会課題

該当するデータがありません

この 技術と関連する公募課題

該当するデータがありません

astavision 新着記事

サイト情報について

本サービスは、国が公開している情報(公開特許公報、特許整理標準化データ等)を元に構成されています。出典元のデータには一部間違いやノイズがあり、情報の正確さについては保証致しかねます。また一時的に、各データの収録範囲や更新周期によって、一部の情報が正しく表示されないことがございます。当サイトの情報を元にした諸問題、不利益等について当方は何ら責任を負いかねることを予めご承知おきのほど宜しくお願い申し上げます。

主たる情報の出典

特許情報…特許整理標準化データ(XML編)、公開特許公報、特許公報、審決公報、Patent Map Guidance System データ