TOP > 国内特許検索 > ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム > 明細書

明細書 :ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム

発行国

日本国特許庁(JP)

公報種別

特許公報(B2)

特許番号

特許第5843230号 (P5843230)

公開番号

特開2013-003897 (P2013-003897A)

登録日

平成27年11月27日(2015.11.27)

発行日

平成28年1月13日(2016.1.13)

公開日

平成25年1月7日(2013.1.7)

発明の名称または考案の名称

ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム

国際特許分類

G06F 17/50 (2006.01)
G06F 11/36 (2006.01)

ＦＩ

G06F 17/50 612L
G06F 17/50 664Z
G06F 9/06 620R

請求項の数または発明の数

全頁数

出願番号

特願2011-135201 (P2011-135201)

出願日

平成23年6月17日(2011.6.17)

審査請求日

平成26年5月30日(2014.5.30)

特許権者または実用新案権者

【識別番号】504132272
【氏名又は名称】国立大学法人京都大学

発明者または考案者

【氏名】末永幸平
【氏名】蓮尾一郎

個別代理人の代理人

【識別番号】110000280、【氏名又は名称】特許業務法人サンクレスト国際特許事務所

審査官

【審査官】加舎理紅子

参考文献・文献

特開２００４－１７８３００（ＪＰ，Ａ）
特開２００３－２７１６７９（ＪＰ，Ａ）
山根智，ハイブリッドシステムの仕様記述言語と形式的検証手法，第４８回システム制御情報学会研究発表講演会講演論文集，２００４年５月２１日，ｐ．３７－４０
足立正和他，同期型言語を用いたソフトウェア検証：クルーズコントロールシステムにおける事例紹介，コンピュータソフトウェア，日本ソフトウェア科学会，２００６年７月２６日，ＶＯＬ．２３，ＮＯ．３，ｐ．８５－９０

調査した分野

Ｇ０６Ｆ１７／５０
Ｇ０６Ｆ１１／３６

特許請求の範囲

【請求項1】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を示す記号が導入されたプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされている
ハイブリッドシステムの検証方法。
【請求項2】
前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項１記載のハイブリッドシステムの検証方法。
【請求項3】
前記検証ステップに先立って、前記モデルのコードにおける無限小を示す前記記号を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証する
請求項１又は２記載のハイブリッドシステムの検証方法。
【請求項4】
前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す記号を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明する
請求項２記載のハイブリッドシステムの検証方法。
【請求項5】
前記数値を表す前記記号は、正の整数を示す記号である
請求項３又は４記載のハイブリッドシステムの検証方法。
【請求項6】
前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含む
請求項１～５のいずれか１項に記載のハイブリッドシステムの検証方法。
【請求項7】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、無限小を示す記号が導入されたプログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備え、
前記モデルは、ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされているハイブリッドシステムの検証装置。
【請求項8】
前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項７記載のハイブリッドシステムの検証装置。
【請求項9】
前記記憶部に記憶されている前記モデルのコードにおける無限小を示す前記記号を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証する
請求項７又は８記載のハイブリッドシステムの検証装置。
【請求項10】
前記検証条件を示す論理式における無限小を示す記号を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明する
請求項８記載のハイブリッドシステムの検証装置。
【請求項11】
前記数値を表す前記記号は、正の整数を示す記号である
請求項９又は１０記載のハイブリッドシステムの検証装置。
【請求項12】
前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備える
請求項７～１１のいずれか１項に記載のハイブリッドシステムの検証装置。
【請求項13】
コンピュータを、請求項７～１２のいずれか１項に記載の検証装置として機能させるためのコンピュータプログラム。
【請求項14】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルをコンピュータにより生成する生成ステップを含み、
前記プログラミング言語は、無限小を示す記号が導入されたプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の微小変化量を、無限小を示す前記記号を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法。
【請求項15】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置あって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を示す記号が導入されたプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の微小変化量を、無限小を示す前記記号を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置。
【請求項16】
コンピュータを、請求項１５記載のモデル変換装置として機能させるためのコンピュータプログラム。
【請求項17】
形式的検証を行うプログラム検証器によって前記形式的検証が行われるコードであって、
前記コードは、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの動作が、無限小を示す記号が導入されたプログラミング言語によってコーディングされたものであり、
前記コードでは、前記ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされている
コード。

発明の詳細な説明

【技術分野】
【0001】
本発明は、ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラムに関するものである。
【背景技術】
【0002】
ハイブリッドシステムは、制御理論における用語であり、速度や温度のような物理量を表す連続値と、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値とが相互に影響を及ぼしあってシステム全体が動作するのが特徴である。
【0003】
典型的なハイブリッドシステムとしては、自動車や航空機など、物理量の制御にソフトウェアが関わるようなシステムが挙げられる。例えば、自動車においては、モータの回転数、ブレーキオイルの圧力、内燃機関での燃焼量といった連続値と、ＡＢＳを動作させるかどうか等の離散値とが、時々刻々と変化しながら自動車の動作を実現している。
このため、ハイブリッドシステムは、連続値のみを扱うプラントや離散値のみを扱うソフトウェアとは異なった複雑さを持っている。
【0004】
ハイブリッドシステムを記述できるシステムとして、ＭａｔｈＷｏｒｋｓ社のＳｉｍｕｌｉｎｋなどがある。
連続的な値のみを扱うシステムを対象とする従来の制御理論では、信号の流れを、図式を用いて表現する手法がよく用いられる。これを計算機上に実現し、さらに離散的な状態変化を表現するブロックを追加して拡張したのが、Ｓｉｍｕｌｉｎｋなどの枠組みである。
【0005】
現在、ハイブリッドシステムの開発現場では、Ｓｉｍｕｌｉｎｋなどの枠組みを利用して、ハイブリッドシステムの開発が行われている。
【先行技術文献】
【0006】

【非特許文献1】インターネット＜ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｍａｔｈｗｏｒｋｓ．ｃｏｍ／ｐｒｏｄｕｃｔｓ／ｓｉｍｕｌｉｎｋ/＞
【発明の概要】
【発明が解決しようとする課題】
【0007】
ここで、ハイブリッドシステムが意図した通りに動作することを検証することは非常に重要な問題である。
一般に、システムが意図した通りに振る舞うことを検証するために、シミュレーションによるテストがよく用いられる。これは、様々な入力をシステムに繰り返し与え、その動作が意図した通りであることを確認することで、システムの品質を担保しようとする手法である。
【0008】
例えば、Ｓｉｍｕｌｉｎｋを用いてハイブリッドシステムの開発を行う場合には、Ｓｉｍｕｌｉｎｋ上で図式によって表現されたハイブリッドシステムに対して、いろいろな信号を入力として与えて、そのハイブリッドシステムの振る舞いをＳｉｍｕｌｉｎｋ上で確認することで、ハイブリッドシステムの品質をチェックすることができる。
【0009】
しかしながら、シミュレーションによるテストに基づく品質チェックのみでは、全ての入力を網羅することが不可能である。したがって、シミュレーションの際に用いなかった入力に対しての品質の担保が全く無い。
【0010】
そこで、本発明は、ハイブリッドシステムの検証のための新たな技術的手段を提供することを目的とする。
【課題を解決するための手段】
【0011】
（１）本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされている
ハイブリッドシステムの検証方法である。
【0012】
（２）前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。
【0013】
（３）前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証するのが好ましい。
【0014】
（４）前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。
【0015】
（５）前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。
【0016】
（６）前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含むのが好ましい。
【0017】
（７）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備えているハイブリッドシステムの検証装置である。
【0018】
（８）前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。
【0019】
（９）前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現形式に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証するのが好ましい。
【0020】
（１０）前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。
【0021】
（１１）前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。
【0022】
（１２）前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備えるのが好ましい。
【0023】
（１３）他の観点からみた本発明は、コンピュータを、前記（７）～（１２）のいずれか１項に記載の検証装置として機能させるためのコンピュータプログラムである。
【0024】
（１４）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法である。
（１５）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置である。
（１６）他の観点からみた本発明は、コンピュータを、前記（１５）のモデル変換装置として機能させるためのコンピュータプログラムである。
【図面の簡単な説明】
【0025】
【図1】ハイブリッドシステムの設計支援及び検証のためのシステムの構成図である。
【図2】貯水槽のモデルを示す図である。
【図3】モデル変換処理のフローチャートである。
【図4】コンピュータ設計支援システムによって作成されたハイブリッドシステムのブロック線図である。
【図5】ブロック線図の結線及びブロックに付与された変数を示す図である。
【図6】変換テーブルを示す図である。
【発明を実施するための形態】
【0026】
以下、本発明の好ましい実施形態について添付図面を参照しながら説明する。

【0027】
［１．ハイブリッドシステムの設計支援及び検証のためのシステム］
図１は、ハイブリッドシステムの設計支援及び検証のためのシステム１を示している。このシステム１は、ハイブリッドシステムの作成を行うことができるコンピュータ支援設計システム２と、コンピュータ支援設計システム２で作成したハイブリッドシステムを、ハイブリッドシステムをモデル化したプログラムに変換する変換器と、プログラミング言語によってコーディングされたハイブリッドシステムを検証する検証装置４と、を備えている。

【0028】
なお、システム１の各機能は、コンピュータの記憶装置にインストールされたコンピュータプログラムが、コンピュータに実行されることによって発揮される。そのコンピュータプログラムは、記録媒体に記録して、譲渡・販売することができる。

【0029】
本実施形態では、ハイブリッドシステムを検証するために、コンピュータ支援設計システム２で作成したハイブリッドシステムに対して、様々な入力を与えてシミュレーションを行うのではなく、プログラムに対する形式的検証を用いて検証を行う。
ここで、プログラム（ソフトウェア）の開発においては、形式的検証（形式的手法によるプログラム検証）による検証が用いられつつある。形式的検証とは、数理科学的に正しさが証明されたアルゴリズム（例えば、定理証明器）で、プログラムを解析し、プログラムにバグが無いことを保証する手法である。なお、形式的検証については、例えば、「林晋、プログラム検証論 (情報数学講座) 、共立出版、１９９４」に開示されている。
形式的検証では、様々な入力を与えてテストすることなく、すべての入力について網羅的にテストを行ったのと同じ結果が得られる。

【0030】
様々な入力を与えてテストすることで検証を行う方法では、システムをモジュール化した場合に、モジュール毎の品質保証ができたとしても、モジュールを組み合わせたシステム全体の品質保証が困難である。しかし、形式的検証には、モジュール毎の品質保証によって、モジュールを組み合わせたシステム全体の品質保証が可能な技術が多く存在するので、モジュール性を確保することが容易である。

【0031】
このように、形式的検証は、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易である。
このように優れた特性を持つ形式的検証の手法を、ハイブリッドシステムの検証に利用するという点が、本発明者らの着想の第一点である。

【0032】
そして、本発明者らの着想の第二点は、プログラミング言語を、ハイブリッドシステムの動作の記述に用いることである。
プログラミング言語は、元来、コンピュータによって実行されるプログラムコードを記述するためのものであり、ハイブリッドシステムの動作を記述するものではない。
従来のプログラミング言語であっても、ハイブリッドシステムの動作のうち、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値の変化は、当然に、記述できる。

【0033】
しかし、ハイブリッドシステムの動作には、ソフトウェアによって制御されるがソフトウェアの動作そのものではない連続値（速度や温度のような物理量）の変化も含まれる。従来、ソフトウェアの動作ではない連続値の変化そのものは、プログラミング言語による記述の対象になっていない。

【0034】
これに対して、本実施形態のシステム１では、ハイブリッドシステムの記述のために拡張されたプログラミング言語が用いられる。その拡張されたプログラミング言語（モデリング言語）によって、連続値の変化を含むハイブリッドシステムの動作が、モデリングされる。そして、拡張されたプログラミング言語を用いてモデリングされたハイブリッドシステムを、プログラム検証技術である形式的検証の手法によって検証する。
これにより、ハイブリッドシステムを、プログラムの検証と同様の手法で検証でき、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易となる。

【0035】
［２．ハイブリッドシステムのモデリング言語］
本実施形態では、手続き型プログラミング言語のエッセンスであるｗｈｉｌｅ言語（ＧｌｙｎｎＷｉｎｓｋｅｌ．ＦｏｒｍａｌＳｅｍａｎｔｉｃｓｏｆＰｒｏｇｒａｍｍｉｎｇＬａｎｇｕａｇｅｓ．ＴｈｅＭＩＴＰｒｅｓｓ，Ｆｅｂｒｕａｒｙ１９９３．）を、無限小の値を表すｄｔという記号で拡張した言語であるｗｈｉｌｅ^ｄｔを用いる。
無限小の値を言語に加えることにより、連続量を扱うシステムを、手続き型プログラミング言語で記述することができる。

【0036】
つまり、プログラミング言語は、元来、ソフトウェアの動作に関わる離散値を記述できるものであるから、無限小の導入によって連続値が記述可能となれば、連続値と離散値とが相互に影響を及ぼしあって変化するハイブリッドシステムの動作が記述可能となる。
なお、無限小を導入したプログラミング言語（ｗｈｉｌｅ^ｄｔ言語）は、コンピュータによる実行を前提としたものではなく、ハイブリッドシステムの動作を記述するための言語である。したがって、無限小を導入したプログラミング言語は、ハイブリッドシステムのモデリング言語ということができる。

【0037】
［２．１モデリング言語ｗｈｉｌｅ^ｄｔの仕様］
以下に、本実施形態で用いられるｗｈｉｌｅ^ｄｔ言語の定義の例を示す。
【数1】

【0038】
ｗｈｉｌｅ^ｄｔ言語の定義は、ＢＮＦ記法で記述されており、例えば、
ａ：：＝ｘ｜ｒ｜ｄｔ｜ａ_１ａｏｐａ_２
は、「ａは、ｘ，ｒ，ｄｔもしくはａ_１ａｏｐａ_２のいずれかである」という意味である。
ａは、算術式で、変数、実数定数、無限小を表す記号ｄｔか、算術演算（ａｏｐ）のいずれかである。
ｂは、真偽値を表す式で、真を表す値、偽を表す値、ブール演算（ａｎｄ演算、ｏｒ演算またはｎｏｔ演算）または算術式間の関係式（ａ_１＜ａ_２等）のいずれかである。

【0039】
ｃはコマンド（プログラムで実行される文）であり、それぞれの意味は以下の
通りである。
ｓｋｉｐ：なにも実行せずに終了する。
ｘ：＝ａ：算術式ａを評価し、その評価結果を変数ｘに代入する。
ｃ１；ｃ２：コマンドｃ_１を実行し、その後コマンドｃ_２を実行する。
ｉｆｂｔｈｅｎｃ_１ｅｌｓｅｃ_２：式ｂを評価し、その結果が真ならばｃ_１を実行し、偽ならばｃ_２を実行する。
ｗｈｉｌｅ^Ｑｂｄｏｃｄｏｎｅ：式ｂが真である間、ｃを繰り返し実行する。

【0040】
上記のように、ｗｈｉｌｅ^ｄｔ言語の定義では、算術式ａの定義に、無限小を示す記号ｄｔが導入されている。無限小を示す記号ｄｔに関する定義の部分を除くと、ｗｈｉｌｅ^ｄｔ言語の定義は、一般的な手続き型プログラミング言語に準拠したものとなっている。
つまり、ｗｈｉｌｅ^ｄｔ言語は、手続き型プログラミング言語を、無限小が記述できるように拡張した言語、ということができる。
なお、ｗｈｉｌｅ^ｄｔ言語の定義は、上記のものに限られず、さらに拡張されていてもよい。本実施形態では、算術演算（ａｏｐ）に累乗を含めるなど、上記定義をさらに拡張したものを用いる。

【0041】
［２．２ｗｈｉｌｅ^ｄｔ言語によるプログラム例（モデル例）］
［例１］
初めに非常にシンプルなｗｈｉｌｅ^ｄｔのプログラム例を示す。このプログラムは微分方程式
【数2】

に従ったｘ(ｔ)の時間発展を時刻５まで計算する。ｗｈｉｌｅコマンドの各ループにおいて、ｘの値は微分方程式で指定された現時刻でのｘの微小変化量(ｘ×ｄｔ)だけ変化する。プログラム中のａｓｓｅｒｔ（ｘ≧２^ａ）は、この時点においてｘ≧２^ａが成り立たなければならないということを表しており、この条件が必ず成り立つことを、後述のプログラム論理を用いて検証する。

【0042】
【数3】

【0043】
［例２］
他の一例として先行研究（ＡｎｄｒｅＰｌａｔｚｅｒ．Ｄｉｆｆｅｒｅｎｔｉａｌｄｙｎａｍｉｃｌｏｇｉｃｆｏｒｈｙｂｒｉｄｓｙｓｔｅｍｓ．Ｊ．Ａｕｔｏｍ．Ｒｅａｓｏｎｉｎｇ，４１（２）:１４３-１８９，２００８．）にて取り上げられているヨーロッパ鉄道制御システム（ＥＴＣＳ）のモデルを挙げる。
Ｃ_{ａｃｃｅｌ}は定数加速度ａで時刻εまで加速する電車をモデル化している。
ここで変数ｖは電車の速度、変数ｚは電車の位置を表現している。ｗｈｉｌｅループで時刻ｔを無限小量ずつ変化させ、コマンドＣ_{ｄｒｉｖｅ}内ではｖ：＝ｖ＋ａ×ｄｔで速度ｖを、加速度ａに応じて変化させ、ｚ：=ｚ+ｖ×ｄｔで電車の位置ｚを現在の速度ｖに応じて変化させている。
【数4】

【0044】
また、以下のプログラムｃ_{ｃｈｋＡｎｄＢｒａｋｅ}は、電車の位置を時間間隔εでモニタリングし、現在の位置が点ｍより距離ｓを越えていることを検知すると加速度を－ｂに変化させ減速し停車する電車をモデル化している。
【数5】

【0045】
［例３］
別の現実に近い例として、先行研究（ＲａｊｅｅｖＡｌｕｒ，ＣｏｓｔａｓＣｏｕｒｃｏｕｂｅｔｉｓ，ＴｈｏｍａｓＡ．Ｈｅｎｚｉｎｇｅｒ， aｎｄＰｅｉ－ＨｓｉｎＨｏ．Ｈｙｂｒｉｄａｕｔｏｍａｔａ：Ａｎａｌｇｏｒｉｔｈｍｉｃａｐｐｒｏａｃｈｔｏｔｈｅｓｐｅｃｉｆｉｃａｔｉｏｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｏｆｈｙｂｒｉｄｓｙｓｔｅｍｓ．ＩｎＨｙｂｒｉｄＳｙｓｔｅｍｓ，ｐａｇｅｓ２０９-２２９，１９９２．）にて取り上げられている貯水槽モニタのモデルを挙げる。
図２に示すように、この貯水槽１００には給水口１０１と排水口１０２が付いており、給水口１０１のバルブ１０３が開いているときは水位が毎秒１ｃｍで上昇し、バルブ１０３が閉じているときには毎秒２ｃｍで下降する。バルブ１０３の操作はスイッチ１０４で行われており、バルブ１０３の開閉はスイッチ１０４の操作後２秒経ってから起こる。

【0046】
この貯水槽をモデル化したのが以下のプログラムｃ_{ｗａｔｅｒ}である。変数ｙは水位を、変数ｘはスイッチ操作からの変化時間を、ｓはスイッチの状態(１＝ｏｎ，０＝ｏｆｆ)を、ｖはバルブ１０３の状態（１＝開，０＝閉）を表している。
以下のプログラムにおいて、ｃａｓｅ｛・・・｝は、初めから順番に条件を検査し、条件が成り立った部分のプログラムを実行する構文である。
【数6】

【0047】
［３．検証装置（プログラム論理を用いた検証アルゴリズム）］
ｗｈｉｌｅ^ｄｔ言語によってコーディングされたハイブリッドシステムのモデルは、プログラミング言語的に記述されているため、形式的検証を行うプログラム検証器４５によって検証が可能である。

【0048】
図１に示すように、検証装置４は、ｗｈｉｌｅ^ｄｔ言語によってコーディングされたハイブリッドシステムのモデルのコード（プログラム）の入力を受け付ける入力部４１を備えている。入力部４１は、システム１内部の他の機能（例えば、図１の変換器３）から、コードの入力を受け付けても良いし、システム１の外部からコードの入力を受け付けても良い。

【0049】
モデルのコード等の入力部４１によって受け付けたデータは、記憶部４２によって記憶される。記憶部４２に記憶されたコード等に対して、検証の前処理を行う処理部（セクション化部４３、ループ不変表明計算部４４）が、所定の前処理を行い、その前処理の結果を、再び、記憶部４２に記憶させる。

【0050】
また、プログラム検証器４５は、記憶部４２に記憶されたコード（必要に応じて前処理の施された後のコード）に対して、形式的検証によって検証を行う。プログラム検証器４５は、検証条件を生成するための検証条件生成器４６と、検証条件として生成された論理式を証明する定理証明器４７と、を有している。
さらに、検証装置４は、定理証明器４７による証明結果（検証結果）を、ハイブリッドシステムの検証結果として出力するための出力部４８を備えている。

【0051】
検証装置４の入力部４１は、検証対象のプログラムのコード（ハイブリッドシステムの動作をｗｈｉｌｅ^ｄｔ言語でコーディングしたコード）ｃと、当該プログラムの実行前に必ず成り立っているべき条件(事前条件)Ｑと、を入力として受け取る。事前条件Ｑは、ハイブリッドシステムの品質を保証するための品質保証条件となる論理式である。なお、品質保証条件は、プログラムの実行後に必ず成り立っているべき条件（事後条件）など、他の条件であってもよい。

【0052】
コードｃ中には、ａｓｓｅｒｔ（Ｑ’）（ただし、Ｑ’は、プログラム変数に関する論理式）という文が各所に記述されている。検証装置４の出力部４８は、与えられた事前条件Ｑが成り立つ状態でプログラムがモデル化しているハイブリッドシステムの実行を開始したと考えた場合に、プログラムｃ中のａｓｓｅｒｔ（Ｑ’）で示された論理式が必ず成り立つならば「検証成功」、成り立たない場合があるならば「検証失敗」を、出力する。

【0053】
検証装置４による検証アルゴリズムにおける具体的な手続きは以下の通りである。
１）プログラムｃ、事前条件Ｑについてセクション化の操作を行う（置換ステップ）。
２）セクション化後のプログラムｃについて、ループ不変表明の計算の操作を行う（付加ステップ）。
３）プログラムｃについて検証条件（論理式）の生成を行う（検証ステップ）。
４）検証条件が成り立つことを、定理証明器を用いて証明する。この証明に定理証明器が成功した場合は検証成功、成功しなかった場合は検証失敗を返す（検証ステップ）。

【0054】
上記のアルゴリズムで検証を行うと、プログラムが与えられた性質を必ず満たすことが数学的に保証される。これにより、ハイブリッドシステムの品質に数学的な保証を与えることができ、ハイブリッドシステムの品質を大きく向上させることが可能となる。

【0055】
以下、検証アルゴリズムの動作について説明する。以下では、説明の簡略化のため、例１のプログラム例についてアルゴリズムの動作を説明するが、例２、例３のプログラムについてもこのアルゴリズムが正しく動くことは確認済みである。

【0056】
［３．１プログラムｃと事前条件Ｑのセクション化］
前記置換ステップでは、セクション化部（置換処理部）４３が、入力として与えられたプログラムｃと事前条件Ｑについてセクション化という操作を行う。セクション化とは、無限小を示す表現であるｄｔを、実数値を示す表現”１／ｉ”に置換する操作である。実数値を示す表現”１／ｉ”は、数値を示す記号”ｉ”を含んでおり、ｉが示す値（の絶対値）が増加したと考えた場合、その増加につれて、表現”１／ｉ”が示す値が０に収束する値を示す表現となっている。つまり、ｉの絶対値が非常に大きくなれば、１／ｉは０に収束する。ここでは、ｉは、正の整数であるとするが、負の整数であってもよい。また、実数値を示す値は、”１／ｉ”に限らず、例えば、”１／（２×ｉ）”または”１／（３×ｉ）”などであってもよい。セクション化の操作によりｗｈｉｌｅ^ｄｔのプログラムｃと事前条件Ｑとが、(無限小の値を含まない)実数上のプログラムｃ_ｉ・論理式Ｑ_ｉに変換される。セクション化により、無限小値を含むプログラムの検証に無限小値を対象としない既存手法（例えば、以下で述べるループ不変表明の計算等）を適用することが可能となる。

【0057】
例として、前記プログラム例１について、
【数7】

のもとでの検証例を見る。

【0058】
この例について、セクション化（置換ステップ）の結果得られるプログラムｃ_ｉと論理式Ｑ_ｉは、次のようになる。
【数8】

【0059】
［３．２ループ不変表明の計算］
前記付加ステップでは、ループ不変表明計算部４４が、セクション化して得られたプログラムｃ_ｉについてループ不変表明（ｌｏｏｐｉｎｖａｒｉａｎｔａｓｓｅｒｔｉｏｎ）を計算し、プログラムｃ_ｉに付加する。

【0060】
ループ不変表明とは、プログラム中のループが、要求される仕様を満たしているか否かを検証するための論理式である。ループ不変表明は、セクション化されたプログラムｃ_ｉ中のループ文において、ループの入口と出口で必ず成り立っているべき論理式として記述される。ループ不変表明計算部４４は、ループ不変表明を構成する論理式を、自動的に生成して、プログラムｃ_ｉ中に付加する。
ループ不変表明を自動生成するアルゴリズムとしては、例えば、ＳｒｉｒａｍＳａｎｋａｒａｎａｒａｙａｎａｎ、ＨｅｎｎｙＢ．Ｓｉｐｍａ，ａｎｄＺｏｈａｒＭａｎｎａ．Ｎｏｎｌｉｎｅａｒｌｏｏｐｉｎｖａｒｉａｎｔｇｅｎｅｒａｔｉｏｎｕｓｉｎｇｇｒｏｅｂｎｅｒｂａｓｅｓ．ＩｎＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ３１ｓｔＡＣＭＳＩＧＰＬＡＮ－ＳＩＧＡＣＴｓｙｍｐｏｓｉｕｍｏｎＰｒｉｎｃｉｐｌｅｓｏｆｐｒｏｇｒａｍｍｉｎｇｌａｎｇｕａｇｅｓ，ＰＯＰＬ ’０４，ｐａｇｅｓ３１８-３２９，ＮｅｗＹｏｒｋ，ＮＹ，ＵＳＡ，２００４．ＡＣＭ．に開示されているものを利用することができる。ループ不変表明の計算・付加は、手動で行っても良い。

【0061】
また、ループ不変表明の計算は、プログラムｃ_ｉに、ｗｈｉｌｅ文などのループ文が含まれている場合には、行う必要があるが、ループ文が含まれていない場合は、行う必要がない。

【0062】
例として、前節のセクション化されたプログラムｃ_ｉについてはループ不変表明として
【数9】

をとることができる。

【0063】
すなわち、ループの入口と出口において、必ずｔ＝ｎ／ｉとｘ＝（１＋１／ｉ）^ｎが成り立つような０以上のｎが存在する。実際に、ｃ_ｉ中のｗｈｉｌｅ文においては初めてループに入る時にはｘ＝１かつｔ＝０が成り立っているので、ｎとして０を取ればループ不変表明は成り立つ。また、ループの入口でループ不変表明が成り立っているときにループ本体を一回実行すると、ｔの値は１／ｉだけ増加し、ｘの値は、（１＋１／ｉ）倍されるので、上記の論理式のｎをｎ＋１と取り直せば、やはりループの出口でもループ不変表明が成り立っている。

【0064】
［３．３検証条件の生成］
プログラム検証器４５の検証条件生成器４６は、記憶部４２に記憶されたプログラム（セクション化され、ループ不変表明が付加されたプログラム）ｃ_ｉ、及び事前条件（セクション化された事前条件）Ｑ_ｉについて、検証条件の生成という手続きを行う。

【0065】
検証条件とは、記述した性質が確かに成り立つための十分条件である。すなわち、生成された検証条件とＱ_ｉが成り立つ状況下でｃ_ｉを実行すると必ずＱ_ｉ’が成り立つ。

【0066】
検証条件生成器４６における検証条件生成アルゴリズムは、プログラム論理と呼ばれる手法に基づいて設計されている。

【0067】
以下に、プログラム論理に基づく検証条件生成アルゴリズムＶＣを示す。
【数10】

【0068】
検証条件生成アルゴリズムＶＣでは、プログラムｃ（セクション化され、ループ不変表明が付加されたプログラム）と、事前条件Ｑを受け取り、検証条件を生成する。
アルゴリズムＶＣは、再帰関数ＶＣ_１を用いて定義されている。
ＶＣ_１（ｃ，Ｑ）は、プログラムｃの実行後に、Ｑが成り立つために、ｃの実行前に成り立っているべき条件を返す。
例えば、ＶＣ_１（ｃ_１；ｃ_２，Ｑ）の定義は、「ＶＣ_１（ｃ_２，Ｑ）の結果をＱ’’、ＶＣ_１（ｃ_１，Ｑ’’）の結果をＱ’としたときに、全体の結果はＱ’である」のように読む。
ＶＣは、「ＶＣ_１によって返された条件が、事前条件から帰結される」ことを意味する論理式を検証条件として返す。
なお、検証条件生成アルゴリズムにおいて、Ｑ［ｘ－＞ａ］は、Ｑ中の変数ｘをａで置き換える操作を示す。

【0069】
プログラム論理に基づく検証条件生成アルゴリズムでは、プログラム全体の検証条件が、その部分プログラムの検証条件の組み合わせで計算されている。これにより、巨大なシステム全体の性質を検証する際に、その構成要素の性質を用いて計算することが容易になる。

【0070】
例１のプログラムについて検証条件生成アルゴリズムＶＣを適用すると、検証条件として以下の論理式が生成される。
【数11】

なお、Ｑ’’（ｔ，ｘ，ｉ）は、ループ不変表明計算部４４によって計算されたループ不変表明である。

【0071】
［３．４定理証明器を用いた検証条件の証明］
前述のように生成された検証条件が、「有限個のｉを除いて正しい」ことが示されれば、元のｗｈｉｌｅ^ｄｔのプログラムｃは、与えられた性質を必ず満たす。この検証条件（論理式）の証明のため、本実施形態では、定理証明器（ＴｈｅｏｒｅｍＰｒｏｖｅｒ）４７を用いる。プログラム検証の分野においては、与えられた論理式が成り立つかどうかを自動的に判定する手法（ＢｅｈｅａｄｓＡｋｂａｒｐｏｕｒａｎｄＬ．Ｃ．Ｐａｕｌｓｏｎ．Ｍｅｔｉｔａｒｓｋｉ：Ａｎａｕｔｏｍａｔｉｃｔｈｅｏｒｅｍｐｒｏｖｅｒｆｏｒｒｅａｌ－ｖａｌｕｅｄｓｐｅｃｉａｌｆｕｎｃｔｉｏｎｓ．Ｊ．ＡｕｔｏｍａｔｅｄＲｅａｓｏｎｉｎｇ，４４（３）：１７５-２０５，２０１０．）や、一部人間の支援によって判定する手法（ＴｈｅＣｏｑＤｅｖｅｌｏｐｍｅｎｔＴｅａｍ．ＲｅｆｅｒｅｎｃｅＭａｎｕａｌ - ＴｈｅＣｏｑＰｒｏｏｆＡｓｓｉｓｔａｎｔ．ＩＮＲＩＡ，２０１０．ｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ／ｒｅｆａｎ／．）が知られており、これらの手法を用いて検証条件が成り立つかどうかを判定する。

【0072】
生成された検証条件をＱ_ｉとすると、前述の「有限個のｉを除いてＱ_ｉが成り立つ」という条件は、論理式を用いて、
【数12】

と書ける。

【0073】
したがって、この論理式を定理証明器で証明することによって、元のプログラム中のａｓｓｅｒｔ（Ｑ）が必ず成り立つことが検証できる。
例１のプログラムについての検証条件を整理すると、
【数13】

が成り立てば、検証条件が成り立つことが分かる。
したがって、定理証明器４７で証明すべき論理式は、
【数14】

となる。この論理式が成り立つことは、定理証明器４７を用いて証明することが可能である。

【0074】
［３．５セクション化について］
上記のアルゴリズムＶＣに先立ちセクション化という操作を行っている。この操作は無限小値を含むプログラムの検証を、実数のみを扱える定理証明器を用いて行うために必要な操作である。本実施形態では、プログラムｃのセクション化を行ってから以降の手続きを行っているが、プログラムｃのセクション化を行わずにループ不変表明の計算と検証条件の生成を行い、その後、検証条件をセクション化して、定理証明器４７に渡しても良い。

【0075】
また、無限小値を直接扱うことのできる定理証明器を用いることが可能な場合は、セクション化を行うことなく検証条件の生成と定理証明器での証明を行うことが可能である。
また、セクション化の手法は、プログラム論理を用いない他の検証手法をｗｈｉｌｅ^ｄｔで記述されたプログラムの検証を行う場合にも有効である。

【0076】
［４．検証例］
［４．１ｗｈｉｌｅ^ｄｔのプログラムの例Ａ］
ｗｈｉｌｅ^ｄｔによってハイブリッドシステムの動作をコーディングしたモデルのプログラムコードＡを、以下に示す。なお、以下のコードにおいて、「＆＆」は、論理積を示す論理演算子である。
【数15】

【0077】
［４．２セクション化］
例Ａのコードをセクション化したコードＡ１を、以下に示す。セクション化により、例Ａのコードに含まれていたｄｔ（無限小を表す記号）が、”１／ｉ”に変換され、無限小ｄｔを含まない形となっている。したがって、既存のソフトウェア検証手法を適用することが可能となっている。
【数16】

【0078】
［４．３ループ不変表明の付加］
セクション化されたコードＡ１に、ループ不変表明を付加したコードＡ２を、以下に示す。
【数17】

【0079】
［４．４検証条件］
セクション化され、かつ、ループ不変表面が付加されたコードＡ２に対し、事前条件をｔｒｕｅとして、検証条件生成アルゴリズムＶＣを適用して得られる検証条件を、以下に示す。この検証条件は、定理証明器Ｃｏｑ（ｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ／ｒｅｆａｎ／）で扱えるフォーマットで記述されている。なお、実際に定理証明器で証明すべき論理式は、以下に示す論理式の先頭に、「ｅｘｉｓｔｓｎ：ｎａｔ，ｉ＞ｎ－＞」を付加したものになる。
【数18】

【0080】
［４．５セクション化せずにループ不変表明を付加］
例ＡのコードＡを、セクション化せずにループ不変表明を付加したコードＡ３を、以下に示す。
【数19】

【0081】
［４．６セクション化せずに生成された検証条件］
セクション化せずにループ不変表明を付加したコードＡ３に対し、事前条件をｔｒｕｅとして、検証条件生成アルゴリズムＶＣを適用して得られる検証条件を、以下に示す。
無限小を直接扱える定理証明器を用いれば、この検証条件の証明を行うことで、コードＡの安全性を示すことができる。無限小を扱える定理証明器としては、（ＴａｎｉａＢｅｄｒａｘ－ＷｅｉｓｓａｎｄＲｏｌａｎｄｏＣｈｕａｑｕｉ，ＩＮＦＭＡＬ：ＡｎＩｎｆｉｎｉｔｅｓｉｍａｌＡｎａｌｙｓｉｓＩｎｔｅｒａｃｔｉｖｅＴｈｅｏｒｅｍＰｒｏｖｅｒａｎｄＰｒｏｂｌｅｍＳｏｌｖｅｒ．ＰｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅＸＩＩＩｎｔｅｒｎａｔｉｏｎａｌＣｏｎｆｅｒｅｎｃｅｏｆｔｈｅＣｈｉｌｅａｎＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅＳｏｃｉｅｔｙ，Ｓａｎｔｉａｇｏ，Ｃｈｉｌｅ，Ｏｃｔｏｂｅｒ１９９２．）に記載のものがある。以下の検証条件中のｄｔを”１／ｉ”で置き換えたものは、［４．４検証条件］で示した検証条件と一致する。
【数20】

【0082】
［５．ｗｈｉｌｅ^ｄｔプログラムへの変換］
図３は、図１に示す変換装置３におけるモデル変換処理を示している。図１に示すように、変換装置３は、生成部３ａと、変換テーブル３ｂと、を備えている。
生成部３ａは、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図（モデル）から、ｗｈｉｌｅ^ｄｔ言語でコーディングされたプログラム（ハイブリッドシステムのモデルのコード）を生成する。
変換テーブル３ｂは、ハイブリッドシステムのブロック線図から、ｗｈｉｌｅ^ｄｔ言語のプログラムコードに生成するために、生成部３ａによって参照される。

【0083】
変換装置３は、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図のデータの入力を受け付けると（ステップＳ１）、コードの生成を開始する。

【0084】
図４は、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図の例を示している。このブロック線図は、時刻１で値が０から１になるステップ信号を生成して出力するブロック５１、入力信号の加減算を行って出力するブロック５２、入力信号を増幅して出力するブロック５３ａ，５３ｂ，５３ｃ、入力信号の積分をして出力するブロック５４ａ，５４ｂ等の各種ブロックを備えている。各ブロックは、結線Ｌ１～Ｌ７によって適宜接続されている。

【0085】
コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図のデータには、ブロック線図中のブロック及び結線を示すデータの他、各ブロックに設定されたパラメータ（例えば、入力信号を増幅して出力するブロック５３ａ，５３ｂ，５３ｃであれば、ゲイン値）を示すデータが含まれている。

【0086】
変換装置３の生成部３ａは、ブロック線図のデータに基づいて、ブロック線図中の各結線Ｌ１～Ｌ７に対応する変数ｘｉ，ｘｉ’（ｉは、自然数）を生成する（ステップＳ２）。なお、途中で分岐する結線は、１本の結線であるとみなす。ここでは、各結線に対して、ｘｉ，ｘｉ’という２つの変数を生成する。
また、生成部３ａは、ブロック線図中の各ブロック５１，５２，５３ａ，５３ｂ，５３ｃ，５４ａ，５４ｂのうち、内部状態を持つブロック５４ａ，５４ｂについて、状態変数ｓｉ，ｓｉ’（ｉは、自然数）を生成する（ステップＳ３）。なお、積分ブロック５４ａ，５４ｂの場合、内部状態を示す値は、積分値である。状態変数についても、各ブロックに対してｓｉ，ｓｉ’という２つの変数が生成される。
図５は、図４のブロック線図に対して、変数生成処理（ステップＳ２，Ｓ３）を行って生成された変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’を示している。

【0087】
さらに、生成部３ａは、時間を表す変数ｔを生成する（ステップＳ４）。
続いて、生成部３ａは、ステップＳ２～４で生成した各変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’，ｔを初期化するコードｃ０を生成する（ステップＳ５）。以下は、各変数を０で初期化したコードｃ０の例を示している。
【数21】

【0088】
なお、ブロックに設定されたパラメータ（ブロック線図のデータ中のパラメータ）として、状態変数の初期値が設定されている場合には、設定された初期値が、生成された変数の初期値となるコードｃ０が生成される。

【0089】
さらに続けて、生成部３ａは、無限小時間後の各変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’の値を計算して変数を更新するためのコードｃ１を生成する（ステップＳ６）。コードｃ１は、コードｃ１１と、コードｃ１２とからなる。

【0090】
コードｃ１１は、各ブロックにおける無限小時間後の出力値として、変数ｘｉに基づいて計算される値を、ｘｉ’に代入するコードである（ここでは、ｘｉのｉと、ｘｉ’のｉとは、一般には異なる値である）。
生成部３ａは、ブロック線図中の各ブロックについて、変換テーブル３ｂを参照することで、コードｃ１１を生成する（ステップＳ６ａ）。なお、変換テーブル３ｂは、変換装置３を構成するコンピュータ又はその他の装置の記憶部に記憶されている。

【0091】
図６は、ブロック線図において用いられるブロックと、ブロックに対応するｗｈｉｌｅ^ｄｔ言語のコードとの対応を規定した変換テーブルの例を示している。なお、図６では、ブロック線図に用いられるブロックとして、Ｓｉｍｕｌｉｎｋで用いられるブロックの一部を例として挙げた。
図６の変換テーブル３ｂの左側が、Ｓｉｍｕｌｉｎｋにおいて用いられるブロックを示しており、変換テーブル３ｂの右側が、各ブロックに対応するｗｈｉｌｅ^ｄｔ言語のコードを示している。

【0092】
生成部３ａが、コードｃ１１を生成する際には、変換テーブル３ｂ中のｗｈｉｌｅ^ｄｔ言語のコードにおける変数を示す記号のうち、ｘｉ，ｘｉ’，ｘｊは、変換対象のブロックの入力又は出力に接続された結線に割り当てられた変数名に置換される。また、変換テーブル３ｂ中のｗｈｉｌｅ^ｄｔ言語のコードにおける変数を示す記号のうち、ｓｉ，ｓｉ’は、置換対象のブロックに割り当てられた状態変数名に置換される。
また、変換テーブル３ｂ中のｗｈｉｌｅ^ｄｔ言語のコードにおけるその他の変数を示す記号（ｄｔを除く）は、置換対象のブロックに設定されたパラメータ（ブロック線図のデータ中のパラメータ）が示す値に置換される。

【0093】
生成部３ａが、図５に示すブロック線図に関して、変換テーブル３ｂを参照することで生成したコードｃ１１を以下に示す。
【数22】

【0094】
コードｃ１２は、ｘｉ’，ｓｉ’の値を、ｘｉ，ｓｉに代入するコードである（ここでは、ｘｉのｉと、ｘｉ’のｉとは同じ値であり、ｓｉのｉと、ｓｉ’のｉも同じ値である）。
生成部３ａが、図５に示すブロック線図に関して、ｘｉ’，ｓｉ’の値を、ｘｉ，ｓｉに代入するコードとして生成したコードｃ１２を以下に示す。
【数23】

【0095】
さらに、生成部３ａは、無限小を示す記号ｄｔを用いて、時間を示す変数ｔを更新するコード（ｗｈｉｌｅ文）を生成し、先に生成したコードｃ０及びコードｃ１を組み合わせて、図５に示すハイブリッドシステムのブロック線図全体の動作を示すコード［ｃ０；ｗｈｉｌｅ（ｔ＜１／ｄｔ）｛ｃ１；ｔ：＝ｔ＋ｄｔ｝］を生成する。

【0096】
生成されたコードは、［ｃ０；ｗｈｉｌｅ（ｔ＜１／ｄｔ）｛ｃ１；ｔ：＝ｔ＋ｄｔ｝］は、コンピュータの記憶部に記憶されて、検証装置４による検証に用いても良いし、表示装置などに出力されてもよい。

【0097】
なお、変換装置３は、上述の変換処理とは逆の変換を行うことで、ブロック線図によって記述可能なハイブリッドシステムの動作を示すｗｈｉｌｅ^ｄｔ言語のコードを、ブロック線図に変換することもできる。

【0098】
なお、本実施形態では、ｗｈｉｌｅ^ｄｔ言語のコードを、変換装置によって自動的に作成したが、人手でコーディングを行っても良い。
さらに、本実施形態では、ハイブリッドシステムの開発者として、ソフトウェア技術者を活用することが可能である。
すなわち、ハイブリッドシステムの開発現場では、制御理論に由来する開発手法が主に採用されているため、通常のソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが困難であった。しかし、本実施形態では、ハイブリッドシステムのモデルを、プログラミング言語によってコーディングできるため、プログラミング言語に慣れているソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが可能である。

【0099】
［６．付記］
なお、上記において開示した事項は、例示であって、本発明を限定するものではなく、様々な変形が可能である。
【符号の説明】
【0100】
１システム
２コンピュータ支援設計システム
３変換装置
３ａ生成部
３ｂ変換テーブル
４検証装置
４１入力部
４２記憶部
４３セクション化部（置換処理部）
４４ループ不変表明計算部
４５プログラム検証器
４６検証条件生成器
４７定理証明器
４８出力部

図面

【図1】	【図2】
【図3】	【図4】
【図5】	【図6】