(57)【要約】【課題】マップを含んだプログラムの不具合を網羅的に検証する装置を提供する。【解決手段】マップを含むプログラムの不具合を検証する装置は、プログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述する記述部（２）と、記述部（２）において記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現するシステム表現部（４）と、プログラムの変数の初期領域と禁止領域とを設定する設定部（１０）と、システム表現部で作成された混合整数／線形システム表現と前記設定された初期領域、禁止領域とに基づいて、初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数を算出する算出部（６）と、算出部（６）においてリャプノフ関数が算出されたか否かに基づいて、プログラムにおける不具合の有無を判定する判定部（８）を備える。【選択図】図１
2009134690.tif 000002
【特許請求の範囲】
【請求項１】
マップを含むプログラムの不具合を検証する装置であって、
前記プログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述する記述部と、
前記記述部において記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現するシステム表現部と、
前記プログラムの変数の初期領域と禁止領域とを設定する設定部と、
前記システム表現部で作成された混合整数／線形システム表現と前記設定された初期領域、禁止領域とに基づいて、前記初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数を算出する算出部と、
前記算出部において前記リャプノフ関数が算出されたか否かに基づいて、前記プログラムにおける不具合の有無を判定する判定部と、を備える、マップを含むプログラムの不具合検証装置。
【請求項２】
請求項１に記載の装置において、前記設定部で設定される禁止領域としてプログラムの変数におけるオーバーフロー領域を設定することによって、前記不具合としてプログラムのオーバーフローを検証する、マップを含むプログラムの不具合検証装置。
【請求項３】
請求項１に記載の装置において、前記設定部で設定される禁止領域としてマップのワインドアップ領域を設定することにより、前記不具合としてプログラムにおけるワインドアップ現象の発生を検証する、マップを含むプログラムの不具合検証装置。
【請求項４】
請求項１乃至３の何れか１項に記載の装置において、前記プログラムはＩｆ−Ｔｈｅｎ分岐、Ｆｏｒループ、Ｗｈｉｌｅループの少なくとも１個を含む、マップを含むプログラムの不具合検証装置。
【請求項５】
マップを含むプログラムの不具合を検証するための方法であって、
前記プログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述するステップと、
前記記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現するステップと、
前記プログラムの変数の初期値で形成される初期領域と変数の禁止領域とを設定するステップと、
前記混合整数／線形システム表現と前記設定された初期領域、禁止領域に基づいて、前記初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数の存在を検出するステップと、
前記検出するステップにおいてリャプノフ関数の存在が検出されない場合、前記プログラムにおいて不具合が存在すると判定するステップと、を備える、マップを含むプログラムの不具合検証方法。
【請求項６】
請求項５に記載の方法において、前記初期領域と変数の禁止領域を設定するステップにおいて、前記禁止領域としてプログラムの変数におけるオーバーフロー領域を設定することによって、前記不具合としてプログラムのオーバーフローを検証する、マップを含むプログラムの不具合検証方法。
【請求項７】
請求項５に記載の方法において、前記初期領域と変数の禁止領域を設定するステップにおいて、前記禁止領域としてマップのワインドアップ領域を設定することにより、前記不具合としてプログラムにおけるワインドアップ現象の発生を検証する、マップを含むプログラムの不具合検証方法。
【請求項８】
請求項５乃至７の何れか１項に記載の方法において、前記プログラムは、Ｉｆ−Ｔｈｅｎ分岐、Ｆｏｒループ、Ｗｈｉｌｅループの少なくとも１個を含む、マップを含むプログラムの不具合検証方法。
【請求項９】
マップを含むプログラムの不具合検証プログラムであって、
前記プログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述する手順と、
前記記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現する手順と、
前記プログラムの変数の初期値で形成される初期領域と変数の禁止領域とを設定する手順と、
前記混合整数／線形システム表現と前記設定された初期領域、禁止領域に基づいて、前記初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数の存在を検出する手順と、
前記検出するステップにおいてリャプノフ関数の存在が検出されない場合、前記プログラムにおいて不具合が存在すると判定する手順と、
をコンピュータに実行させる、マップを含むプログラムの不具合検証プログラム。
【請求項１０】
請求項９に記載のプログラムであって、前記初期領域と変数の禁止領域を設定する手順において、前記禁止領域としてプログラムの変数におけるオーバーフロー領域を設定することによって、前記不具合としてプログラムのオーバーフローを検証する、マップを含むプログラムの不具合検証プログラム。
【請求項１１】
請求項９に記載のプログラムであって、前記初期領域と変数の禁止領域を設定する手順において、前記禁止領域としてマップのワインドアップ領域を設定することにより、前記不具合としてプログラムにおけるワインドアップ現象の発生を検証する、マップを含むプログラムの不具合検証プログラム。
【請求項１２】
請求項９乃至１１の何れか１項に記載のプログラムにおいて、前記プログラムは、Ｉｆ−Ｔｈｅｎ分岐、Ｆｏｒループ、Ｗｈｉｌｅループの少なくとも１個を含む、マップを含むプログラムの不具合検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムの不具合検証装置、検証方法、検証プログラムに関し、特に、マップを含むプログラムのオーバーフローまたはワインドアップ現象の発生を検証するための装置、方法およびプログラムに関する。
【背景技術】
【０００２】
プログラムの不具合を検証するためには、通常、プログラムに対してテスト用に作成した特定の信号を入力して、そのプログラムの挙動、例えばオーバーフローが存在するか否かを確かめることが行われている。しかしながらこのようなテストベースの検証方法では、入力したテストデータに依存した検証結果が得られることとなり、一方で、テストデータがプログラムの全動作パターンを網羅しうるものか否かを判定する手段は存在しない。その結果、このような検証方法では潜在的なプログラムミスを見逃してしまう恐れがある。
【０００３】
最近、Ｉｆ−Ｔｈｅｎ分岐やＦｏｒループ等を含むプログラムに対して、プログラムを混合整数／線形システムで表現して、システムの変数と初期領域および禁止領域間にリャプノフ関数（Ｌｙａｐｕｎｏｖ−ｌｉｋｅ関数）が成立するか否かにより、プログラムにオーバーフローが発生するか否かを判定する手法が提案されている（非特許文献１参照）。リャプノフ関数は、変数の初期領域と禁止領域の境界線であり、このようなリャプノフ関数が算出されると初期領域から禁止領域への遷移は発生せず、従って、プログラムにオーバーフローが無いと判断される。
【０００４】
プログラムの混合整数／線形システム表現およびリャプノフ関数を用いる上記のオーバーフロー検証方法では、テスト入力信号、即ち外部入力に依存しない検証結果を得ることができ、理論的にプログラムの全動作パターンを網羅して、オーバーフロー検証を行うことが可能となる。
【０００５】
【非特許文献１】「Ｍｏｄｅｌｉｎｇ，  Ｏｐｔｉｍｉｚａｔｉｏｎ  ａｎｄ  Ｃｏｍｐｕｔａｔｉｏｎ  ｆｏｒ  Ｓｏｆｔｗａｒｅ  Ｖｅｒｉｆｉｃａｔｉｏｎ」Ｍ．Ｒｏｏｚｂｅｈａｎｉ  ｅｔ．ａｌ．，  ＨＳＣＣ  ２００５，Ｌｅｃｔｕｒｅ  Ｎｏｔｅ  ｏｎ  Ｃｏｍｐｕｔｅｒ  Ｓｃｉｅｎｃｅ  ３４１４，ｐｐ．６０６−６２２，２００５
【発明の開示】
【発明が解決しようとする課題】
【０００６】
自動車のエンジン制御には、例えば、空燃比制御マップ、点火時期マップのような制御マップを大量に使用する。上記非特許文献に記載の従来技術では、プログラムにおけるマップの存在を陽に考慮していないので、この技術を用いてマップを含むプログラムの不具合、例えばオーバーフローあるいはワインドアップ現象の発生を検証することができない。
【０００７】
本発明は、従来技術のこのような問題を解決する目的でなされたもので、テスト入力を用いることなく、マップを含むプログラムの不具合の検証が可能な装置、方法、プログラムを提供することを、その課題とする。
【課題を解決するための手段】
【０００８】
上記課題を解決するために、本発明のマップを含むプログラムの不具合検証装置は、検証対象であるプログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述する記述部と、前記記述部において記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現するシステム表現部と、前記プログラムの変数の初期領域と禁止領域とを設定する設定部と、前記システム表現部で作成された混合整数／線形システム表現と前記設定された初期領域、禁止領域とに基づいて、前記初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数を算出する算出部と、前記算出部において前記リャプノフ関数が算出されたか否かに基づいて、前記プログラムにおける不具合の有無を判定する判定部と、を備える。
【０００９】
本発明のマップを含むプログラムの不具合を検証するための方法は、検証対象であるプログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述するステップと、前記記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現するステップと、前記プログラムの変数の初期値で形成される初期領域と変数の禁止領域とを設定するステップと、前記混合整数／線形システム表現と前記設定された初期領域、禁止領域に基づいて、前記初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数の存在を検出するステップと、前記検出するステップにおいてリャプノフ関数の存在が検出されない場合、前記プログラムにおいて不具合が存在すると判定するステップと、を備える。
【００１０】
本発明のマップを含むプログラムの不具合を検証するためのプログラムは、検証対象であるプログラム中のマップを分解してＩｆ−Ｔｈｅｎ分岐により記述するステップと、前記記述されたＩｆ−Ｔｈｅｎ分岐を含めて前記プログラムを混合整数／線形システムとして表現するステップと、前記プログラムの変数の初期値で形成される初期領域と変数の禁止領域とを設定するステップと、前記混合整数／線形システム表現と前記設定された初期領域、禁止領域に基づいて、前記初期領域から前記禁止領域への到達不可能性を補償するリャプノフ関数の存在を検出するステップと、前記検出するステップにおいてリャプノフ関数の存在が検出されない場合、前記プログラムにおいて不具合が存在すると判定するステップと、をコンピュータに実行させる。
【００１１】
上記装置、方法、プログラムにおいて、前記禁止領域としてプログラムの変数におけるオーバーフロー領域を設定することにより、前記不具合としてプログラムのオーバーフローの有無を検証することができる。また、前記禁止領域としてマップのワインドアップ領域を設定することにより、前記不具合としてプログラムにおけるワインドアップ現象の発生を検証することができる。
【００１２】
なお、上記装置、方法、プログラムにおいて、前記検証対象であるマップを含むプログラムは、Ｉｆ−Ｔｈｅｎ分岐、Ｆｏｒループ、Ｗｈｉｌｅループの少なくとも１個を含んで記載されていても良い。
【発明の効果】
【００１３】
マップを含むプログラムの検証において、一般には検証対象のプログラムに対して外部入力を印加してそのプログラムの挙動を確かめることが行われる。しかしながら、このようなテスト入力に依存する検証では、プログラムの可能な全ての動作パターンを網羅するテスト入力を作成することは事実上不可能であり、そのため、潜在的なプログラムミスを見逃してしまう恐れが常に存在する。
【００１４】
これに対して、本発明の装置、方法、プログラムによれば、マップをＩｆ−Ｔｈｅｎ分岐で記述することによって、マップを含むプログラム全体を混合整数／線形システム表現に変換することができるので、この表現に対して変数の初期領域および禁止領域を設定してその間の境界を示すリャプノフ関数を算出し、リャプノフ関数の存在性を確認する。プログラムにおける不具合の発生の有無は、リャプノフ関数の存在の有無によって決定される。従ってこの手法では、テスト入力に依存せず、理論的にプログラムの全パターンを網羅する検証を行うことができるので、潜在的なプログラムミスの発生を防止することができる。
【発明を実施するための最良の形態】
【００１５】
以下に、本発明の一実施形態について図面を参照して説明する。
【００１６】
図１は、本発明の一実施形態に係るマップを含むプログラムの不具合検証装置１の概略構成を示すブロック図であり、図２は、図１に示す装置の動作手順を示すフローチャートである。図１に示す装置は、プログラムの不具合として、プログラムのオーバーフローを検証するためのオーバーフロー検証装置（以下、検証装置）である。検証装置１は、マップのＩｆ−Ｔｈｅｎ分岐記述部（以下、記述部）２、混合整数／線形システム表現変換部（以下、変換部）４、リャプノフ関数（Ｌｙａｐｕｎｏｖ−ｌｉｋｅ関数）算出部（以下、算出部）６、オーバーフロー判定部８および変数の初期領域・禁止領域設定部（以下、領域設定部）１０を備えて構成される。
【００１７】
図１に示すように、記述部２には外部よりマップの情報が入力される。また、領域設定部１０には、外部より、マップの変数の変域から決定される初期領域、禁止領域に関する情報が入力される。オーバーフローが発生するか否かを示す判定結果はオーバーフロー判定部８より出力される。
【００１８】
以下、図２のフローチャートを参照して図１に示す装置の構成および動作を説明する。まずステップＳ２において、記述部２は入力されたマップの情報を分解して、Ｉｆ−Ｔｈｅｎ分岐で記述する。
【００１９】
図３および図４は、オーバーフローを検証しようとするプログラムに含まれるマップ２０をＩｆ−Ｔｈｅｎ形式で表す一例を示している。図３に示すように、ある１次元入力ｕの前回値ｕ（ｋ−１）（ｋはステップ数を示す）を引数として、ある出力ｙの出力値ｙ（ｋ）をマップ２０を用いて計算することを考える。この場合、マップ２０は、例えば、図４に示すように、Ｉｆ−Ｔｈｅｎ形式のプログラムとして記述することが可能である。従って、図１の検証装置１では、プログラム中に含まれているマップの部分をＩｆ−Ｔｈｅｎ形式のプログラムとして記述する。
【００２０】
プログラムのマップ以外の部分は、Ｉｆ−Ｔｈｅｎ分岐、Ｆｏｒループ、Ｗｈｉｌｅループを含んで構成される。ステップＳ２でマップがＩｆ−Ｔｈｅｎ分岐として表現されると、Ｉｆ−Ｔｈｅｎ分岐、Ｆｏｒループ、Ｗｈｉｌｅループを含むプログラム全体を混合整数／線形システム表現に変換することが可能となる。この変換処理（ステップＳ４）は、図１の変換部４において行われる。
【００２１】
混合整数／線形システム表現は、以下の式で示される。
【００２２】
【数１】
2009134690.tif 000003
【００２３】
ここで、
ｋ：ステップ数
ｚ（ｋ）：連続変数をまとめたベクトル
ｗ（ｋ）：連続な補助変数をまとめたベクトル
ｖ（ｋ）：｛０，１｝のどちらかを取る離散変数をまとめたベクトル
Ｆ，Ｈ：関数
を示す。
【００２４】
上記の関数Ｆ，Ｈおよびベクトルを適宜に設定することによって、プログラムと等価な数式表現を得ることができる（非特許文献１参照）。
【００２５】
次に、図３に示すマップ２０、図４に示すマップ２０のＩｆ−Ｔｈｅｎ分岐表現を例として、混合整数／線形システム表現の作成手順について説明する。
【００２６】
今、簡単のため、マップ２０の数値が以下の表１に示す様に与えられているものとする。また、入力変数の変域が−２０〜２０までに制限されているとする。
【００２７】
【表１】
2009134690.tif 000004
【００２８】
ここで、バイナリ変数δ１、δ２、δ３を導入し、以下のとおり定義する。
【数２】
2009134690.tif 000005
【００２９】
このとき、入力ｕ（ｋ−１）がマップのどの区間に存在するかを意味するバイナリ変数δ０１、δ１２、δ２３、δ３４は次式より与えられる。
【数３】
2009134690.tif 000006
【００３０】
また、補助変数ｗ１、ｗ２、ｗ３、ｗ４を以下のとおり、定める。
【数４】
2009134690.tif 000007
【００３１】
変数間の全ての関係を列挙すると以下のとおりになる。但し、ｘは中間変数である。
【数５】
2009134690.tif 000008
【００３２】
ベクトルｚ、ｗ、ｖの定義は以下のとおりである。
【数６】
2009134690.tif 000009
【００３３】
従って、ベクトルｚ、ｗ、ｖを定義し、係数行列Ａ、Ｂ１、Ｂ２、Ｅ１、Ｅ２、Ｅ３、Ｅ４を図５に示す式から定めれば、混合整数／線形システムとして記述できる。なお、図５は、変数間の全ての関係を列挙した表である。混合整数／線形システム表現は、以下の式で示される。
【００３４】
【数７】
2009134690.tif 000010
【００３５】
なお、このシステム表現を得るためのツールは、下記のＷＥＢから入手可能である。
http://control.ee.ethz.ch/~hybrid/hysdel/
【００３６】
以上のようにして、マップを含むプログラムが混合整数／線形システム表現に変換されると、次のステップＳ６（図２）で、変数の初期領域および禁止領域に関する情報が取得される。この情報は、プログラムの変数の初期値および禁止領域の情報に基づいて、変数の初期領域・禁止領域の設定部１０（図１参照）において算出される。
【００３７】
次のステップＳ８では、混合整数／線形システムと変数の初期領域および禁止領域からリャプノフ関数が求められる。リャプノフ関数の算出は、図１のリャプノフ関数算出部において行われる。リャプノフ関数は、図６に示すように、初期領域と禁止領域との間の越すことのできない境界線を示す。この関数は、行列不等式の可解問題を解くことにより、その存在性が確認できる。
【００３８】
従って、ステップＳ１０でリャプノフ関数が存在するか否かを判定し、存在する場合（ステップＳ１０のＹＥＳ）、プログラムにオーバーフローが発生しないと判定する（ステップＳ１２）。リャプノフ関数が存在しないと判定されると（ステップＳ１０のＮＯ）、プログラムにオーバーフローが発生すると判定される（ステップＳ１４）。ステップＳ１０で行われるリャプノフ関数の存在性の確認、およびその確認に基づくオーバーフローの存在の判定は、図１のオーバーフロー判定部８で行われる。
【００３９】
以上のようにして、プログラムがマップを含む場合でも、理論的にプログラムの全パターンを網羅する検証結果を得ることができる。
【００４０】
なお、図１に示すブロック図は、機能を中心として装置の構成を示しているが、図示の構成要素のそれぞれは、実際はプログラムとして図７に示すようなコンピュータシステムに組み込まれ、実行される。
【００４１】
図７のコンピュータシステムについて、簡単に説明する。本実施形態に係るマップを含むプログラムのオーバーフロー検証装置７０は、ＣＰＵ７２、メインメモリ７４、外部記憶装置７６、入力装置７８、出力装置８０、およびＣＰＵ７２とメインメモリ７４、外部記憶装置７６、入力装置７８および出力装置８０間を接続するバス８２、を含んで構成される。
【００４２】
ＣＰＵ７２は中央演算装置であって、入力装置７８と外部記憶装置７６から、プログラムのオーバーフロー判定に必要なデータを入力し、外部記憶装置７６に格納されている本実施形態のプログラムをメインメモリ７４にロードして実行する。即ち、ＣＰＵ７２は、このプログラムを実行して、マップのＩｆ−Ｔｈｅｎ分岐記述、プログラムの混合整数／線形システム表現への変換、リャプノフ関数の算出等を行う。
【００４３】
メインメモリ７４は、本実施形態のオーバーフロー検証プログラムが外部記憶装置７６からロードされる領域を有すると共に、それらの処理で必要となる作業領域を有するメモリである。外部記憶装置７６は、本実施形態のプログラムを格納すると共に、本実施形態のプログラムの実行に必要なデータ、さらにプログラムの実行によって作成される各種データを格納する。
【００４４】
入力装置７８は、プログラムの実行に必要なデータを入力するための装置であり、キーボードやマウスなどのポインティングデバイスなどから構成される。出力装置８０は、外部記憶装置７６に保存されている種々のデータや本実施形態のプログラムの処理結果などを出力する装置であり、ディスプレイやプリンタなどから構成される。なお、本装置は、基本的に図２のフローチャートに沿ってプログラムのオーバーフロー検証を実行する。
【００４５】
以下に、本発明の第二の実施形態について図面を参照して説明する。
【００４６】
図８は、例えばエンジン制御等で使用されるマップにおける、外挿領域を説明するための図である。マップは、ある範囲のマップ引数に対して測定によりあるいは計算によってマップ出力を特定することにより形成されるが、外挿領域は、マップの形成範囲を超えた領域を示す。マップを使用する制御系において、外挿領域に該当するマップ引数が長く選択されると、制御系のワインドアップ現象が発生する。ワインドアップ現象とは、制御入力の飽和によるオーバーシュートなどの制御性能の劣化現象であり、最悪の場合、制御系の不安定化を招く。
【００４７】
図９は、制御系におけるワインドアップ状態を説明するための図である。図９の（ａ）は、制御時のマップ出力の時間変化を示し、図（ｂ）はマップ出力に対応する制御系の出力の時間変化を示している。図９（ａ）で、点線ａおよびｂは外挿領域限界を示している。今、図９（ａ）のサークルｃで示す様に、マップ出力が外挿領域限界に一定時間達すると、制御系の出力は、図９（ｂ）に示す様に、制御によって維持すべき値Ａを超えて不安定な状態、即ち、ワインドアップ状態となる。
【００４８】
図１０は、本発明の第二の実施形態に係るマップを含むプログラムのワインドアップ検証装置１００の概略構成を示すブロック図であり、図１１は、図１０に示す装置の動作手順を示すフローチャートである。図１０に示すように、プログラムのワインドアップ検証装置（以下、検証装置）１００は、マップのＩｆ−Ｔｈｅｎ分岐記述部（以下、記述部）１０２、混合整数／線形システム表現変換部（以下、変換部）１０４、リャプノフ関数（Ｌｙａｐｕｎｏｖ−ｌｉｋｅ関数）算出部（以下、算出部）１０６、ワインドアップ判定部１０８および変数の初期領域・禁止領域の設定部（以下、領域設定部）１１０を備えて構成される。
【００４９】
以下、図１１のフローチャートを参照して図１０に示す装置の構成および動作を説明する。まず、ステップＳ２０において、記述部１０２は入力されたマップの情報を分解して、Ｉｆ−Ｔｈｅｎ分岐で記述する。ステップＳ２２では、変換部１０４においてプログラム全体を混合整数／線形システム表現に変換する。なお、記述部１０２、変換部１０４の構成およびステップＳ２０、Ｓ２２の詳細は、第一の実施形態の記述部２、変換部４およびステップＳ２、Ｓ４と同じであるので、その説明は省略する。
【００５０】
以上のようにして、マップを含むプログラムが混合整数／線形システム表現に変換されると、次のステップＳ２４（図１１）で、変数の初期領域およびワインドアップ領域（外挿領域）に関する情報が取得される。この情報は、プログラムの変数の初期値および外挿領域の情報に基づいて、変数の初期領域・禁止領域の設定部１１０（図１０参照）において算出される。
【００５１】
次のステップＳ２８では、混合整数／線形システムと変数の初期領域およびワインドアップ領域からリャプノフ関数が求められる。リャプノフ関数の算出は、図１０のリャプノフ関数算出部１０６において行われる。リャプノフ関数は、図６に示すように、初期領域とワインドアップ領域（図６の禁止領域に対応）との間の越すことのできない境界線を示す。この関数は、行列不等式の可解問題を解くことにより、その存在性が確認できる。
【００５２】
従って、ステップＳ２８でリャプノフ関数が存在するか否かを判定し、存在する場合（ステップＳ２８のＹＥＳ）、このプログラムにおいてワインドアップ現象が発生しないと判定する（ステップＳ３０）。ステップＳ２８でリャプノフ関数が存在しないと判定されると（ステップＳ２８のＮＯ）、このプログラムにおいてワインドアップ現象が発生すると判定する（ステップＳ３２）。ステップＳ２８で行われるリャプノフ関数の存在性の確認、およびその確認に基づくワインドアップ現象の発生の有無の判定は、図１０のワインドアップ判定部１０８で行われる。
【００５３】
以上のようにして、プログラムがマップを含む場合でも、ワインドアップ現象の発生に関して、理論的にプログラムの全パターンを網羅する検証結果を得ることができる。なお、図１０に示す装置も、第一の実施形態の場合と同様に、図７に示すコンピュータシステムに組み込まれ、実行される。
【図面の簡単な説明】
【００５４】
【図１】本発明の一実施形態に係る装置の概略構成を示すブロック図。
【図２】図１に示す装置の動作説明のためのフローチャート。
【図３】マップの一例を示す図。
【図４】マップをＩｆ−Ｔｈｅｎ分岐で記述した結果を示す図。
【図５】プログラムを混合整数／線形システム表現に変換する場合の説明に供する図であって、変数間の全ての関係を列挙する図。
【図６】リャプノフ関数を説明するための図。
【図７】本発明の一実施形態としてのプログラムを実行するコンピュータシステムの構成を示す図。
【図８】マップにおける外挿領域を説明するための図。
【図９】マップ出力とワインドアップ状態発生の関係を示す図。
【図１０】本発明の第二の実施形態に係る装置の概略構成を示すブロック図。
【図１１】図１０に示す装置の動作説明のためのフローチャート。
【符号の説明】
【００５５】
１    マップを含むプログラムのオーバーフロー検証装置
２    マップのＩｆ−Ｔｈｅｎ分岐記述部
４    混合整数／線形システム表現変換部
６    リャプノフ関数算出部
８    オーバーフロー判定部
１０    変数の初期領域・禁止領域の設定部
１００    マップを含むプログラムのワインドアップ検証装置
１０２    マップのＩｆ−Ｔｈｅｎ分岐記述部
１０４    混合整数／線形システム表現変換部
１０６    リャプノフ関数算出部
１０８    ワインドアップ判定部
１１０    変数の初期領域・ワインドアップ領域の設定部
【図１】
2009134690.tif 000011
【図２】
2009134690.tif 000012
【図３】
2009134690.tif 000013
【図４】
2009134690.tif 000014
【図５】
2009134690.tif 000015
【図６】
2009134690.tif 000016
【図７】
2009134690.tif 000017
【図８】
2009134690.tif 000018
【図９】
2009134690.tif 000019
【図１０】
2009134690.tif 000020
【図１１】
2009134690.tif 000021