ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム
【課題】ハイブリッドシステムの検証を、ソフトウェア検証の手法で行えるようにする。
【解決手段】 連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、モデルのコードを、形式的検証を行うプログラム検証器４５によって検証することで、ハイブリッドシステムの検証を行う検証ステップと、を含んでいる。プログラミング言語は、無限小を記述可能なプログラミング言語である。モデルは、ハイブリッドシステムにおける連続値の変化が、前記無限小を用いてコーディングされている。
【解決手段】 連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、モデルのコードを、形式的検証を行うプログラム検証器４５によって検証することで、ハイブリッドシステムの検証を行う検証ステップと、を含んでいる。プログラミング言語は、無限小を記述可能なプログラミング言語である。モデルは、ハイブリッドシステムにおける連続値の変化が、前記無限小を用いてコーディングされている。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラムに関するものである。
【背景技術】
【０００２】
ハイブリッドシステムは、制御理論における用語であり、速度や温度のような物理量を表す連続値と、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値とが相互に影響を及ぼしあってシステム全体が動作するのが特徴である。
【０００３】
典型的なハイブリッドシステムとしては、自動車や航空機など、物理量の制御にソフトウェアが関わるようなシステムが挙げられる。例えば、自動車においては、モータの回転数、ブレーキオイルの圧力、内燃機関での燃焼量といった連続値と、ＡＢＳを動作させるかどうか等の離散値とが、時々刻々と変化しながら自動車の動作を実現している。
このため、ハイブリッドシステムは、連続値のみを扱うプラントや離散値のみを扱うソフトウェアとは異なった複雑さを持っている。
【０００４】
ハイブリッドシステムを記述できるシステムとして、ＭａｔｈＷｏｒｋｓ社のＳｉｍｕｌｉｎｋなどがある。
連続的な値のみを扱うシステムを対象とする従来の制御理論では、信号の流れを、図式を用いて表現する手法がよく用いられる。これを計算機上に実現し、さらに離散的な状態変化を表現するブロックを追加して拡張したのが、Ｓｉｍｕｌｉｎｋなどの枠組みである。
【０００５】
現在、ハイブリッドシステムの開発現場では、Ｓｉｍｕｌｉｎｋなどの枠組みを利用して、ハイブリッドシステムの開発が行われている。
【先行技術文献】
【非特許文献】
【０００６】
【非特許文献１】インターネット＜ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｍａｔｈｗｏｒｋｓ．ｃｏｍ／ｐｒｏｄｕｃｔｓ／ｓｉｍｕｌｉｎｋ/＞
【発明の概要】
【発明が解決しようとする課題】
【０００７】
ここで、ハイブリッドシステムが意図した通りに動作することを検証することは非常に重要な問題である。
一般に、システムが意図した通りに振る舞うことを検証するために、シミュレーションによるテストがよく用いられる。これは、様々な入力をシステムに繰り返し与え、その動作が意図した通りであることを確認することで、システムの品質を担保しようとする手法である。
【０００８】
例えば、Ｓｉｍｕｌｉｎｋを用いてハイブリッドシステムの開発を行う場合には、Ｓｉｍｕｌｉｎｋ上で図式によって表現されたハイブリッドシステムに対して、いろいろな信号を入力として与えて、そのハイブリッドシステムの振る舞いをＳｉｍｕｌｉｎｋ上で確認することで、ハイブリッドシステムの品質をチェックすることができる。
【０００９】
しかしながら、シミュレーションによるテストに基づく品質チェックのみでは 、全ての入力を網羅することが不可能である。したがって、シミュレーションの際に用いなかった入力に対しての品質の担保が全く無い。
【００１０】
そこで、本発明は、ハイブリッドシステムの検証のための新たな技術的手段を提供することを目的とする。
【課題を解決するための手段】
【００１１】
（１）本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされている
ハイブリッドシステムの検証方法である。
【００１２】
（２）前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。
【００１３】
（３）前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証するのが好ましい。
【００１４】
（４）前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。
【００１５】
（５）前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。
【００１６】
（６）前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含むのが好ましい。
【００１７】
（７）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備えているハイブリッドシステムの検証装置である。
【００１８】
（８）前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。
【００１９】
（９）前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現形式に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証するのが好ましい。
【００２０】
（１０）前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。
【００２１】
（１１）前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。
【００２２】
（１２）前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備えるのが好ましい。
【００２３】
（１３）他の観点からみた本発明は、コンピュータを、前記（７）〜（１２）のいずれか１項に記載の検証装置として機能させるためのコンピュータプログラムである。
【００２４】
（１４）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法である。
（１５）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置である。
（１６）他の観点からみた本発明は、コンピュータを、前記（１５）のモデル変換装置として機能させるためのコンピュータプログラムである。
【図面の簡単な説明】
【００２５】
【図１】ハイブリッドシステムの設計支援及び検証のためのシステムの構成図である。
【図２】貯水槽のモデルを示す図である。
【図３】モデル変換処理のフローチャートである。
【図４】コンピュータ設計支援システムによって作成されたハイブリッドシステムのブロック線図である。
【図５】ブロック線図の結線及びブロックに付与された変数を示す図である。
【図６】変換テーブルを示す図である。
【発明を実施するための形態】
【００２６】
以下、本発明の好ましい実施形態について添付図面を参照しながら説明する。
【００２７】
［１．ハイブリッドシステムの設計支援及び検証のためのシステム］
図１は、ハイブリッドシステムの設計支援及び検証のためのシステム１を示している。このシステム１は、ハイブリッドシステムの作成を行うことができるコンピュータ支援設計システム２と、コンピュータ支援設計システム２で作成したハイブリッドシステムを、ハイブリッドシステムをモデル化したプログラムに変換する変換器と、プログラミング言語によってコーディングされたハイブリッドシステムを検証する検証装置４と、を備えている。
【００２８】
なお、システム１の各機能は、コンピュータの記憶装置にインストールされたコンピュータプログラムが、コンピュータに実行されることによって発揮される。そのコンピュータプログラムは、記録媒体に記録して、譲渡・販売することができる。
【００２９】
本実施形態では、ハイブリッドシステムを検証するために、コンピュータ支援設計システム２で作成したハイブリッドシステムに対して、様々な入力を与えてシミュレーションを行うのではなく、プログラムに対する形式的検証を用いて検証を行う。
ここで、プログラム（ソフトウェア）の開発においては、形式的検証（形式的手法によるプログラム検証）による検証が用いられつつある。形式的検証とは、数理科学的に正しさが証明されたアルゴリズム（例えば、定理証明器）で、プログラムを解析し、プログラムにバグが無いことを保証する手法である。なお、形式的検証については、例えば、「林 晋、プログラム検証論 (情報数学講座) 、共立出版、１９９４」に開示されている。
形式的検証では、様々な入力を与えてテストすることなく、すべての入力について網羅的にテストを行ったのと同じ結果が得られる。
【００３０】
様々な入力を与えてテストすることで検証を行う方法では、システムをモジュール化した場合に、モジュール毎の品質保証ができたとしても、モジュールを組み合わせたシステム全体の品質保証が困難である。しかし、形式的検証には、モジュール毎の品質保証によって、モジュールを組み合わせたシステム全体の品質保証が可能な技術が多く存在するので、モジュール性を確保することが容易である。
【００３１】
このように、形式的検証は、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易である。
このように優れた特性を持つ形式的検証の手法を、ハイブリッドシステムの検証に利用するという点が、本発明者らの着想の第一点である。
【００３２】
そして、本発明者らの着想の第二点は、プログラミング言語を、ハイブリッドシステムの動作の記述に用いることである。
プログラミング言語は、元来、コンピュータによって実行されるプログラムコードを記述するためのものであり、ハイブリッドシステムの動作を記述するものではない。
従来のプログラミング言語であっても、ハイブリッドシステムの動作のうち、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値の変化は、当然に、記述できる。
【００３３】
しかし、ハイブリッドシステムの動作には、ソフトウェアによって制御されるがソフトウェアの動作そのものではない連続値（速度や温度のような物理量）の変化も含まれる。従来、ソフトウェアの動作ではない連続値の変化そのものは、プログラミング言語による記述の対象になっていない。
【００３４】
これに対して、本実施形態のシステム１では、ハイブリッドシステムの記述のために拡張されたプログラミング言語が用いられる。その拡張されたプログラミング言語（モデリング言語）によって、連続値の変化を含むハイブリッドシステムの動作が、モデリングされる。そして、拡張されたプログラミング言語を用いてモデリングされたハイブリッドシステムを、プログラム検証技術である形式的検証の手法によって検証する。
これにより、ハイブリッドシステムを、プログラムの検証と同様の手法で検証でき、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易となる。
【００３５】
［２． ハイブリッドシステムのモデリング言語］
本実施形態では、手続き型プログラミング言語のエッセンスであるｗｈｉｌｅ言語（Ｇｌｙｎｎ Ｗｉｎｓｋｅｌ． Ｆｏｒｍａｌ Ｓｅｍａｎｔｉｃｓ ｏｆ Ｐｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ． Ｔｈｅ ＭＩＴ Ｐｒｅｓｓ， Ｆｅｂｒｕａｒｙ １９９３．）を、無限小の値を表すｄｔという記号で拡張した言語であるｗｈｉｌｅｄｔを用いる。
無限小の値を言語に加えることにより、連続量を扱うシステムを、手続き型プログラミング言語で記述することができる。
【００３６】
つまり、プログラミング言語は、元来、ソフトウェアの動作に関わる離散値を記述できるものであるから、無限小の導入によって連続値が記述可能となれば、連続値と離散値とが相互に影響を及ぼしあって変化するハイブリッドシステムの動作が記述可能となる。
なお、無限小を導入したプログラミング言語（ｗｈｉｌｅｄｔ言語）は、コンピュータによる実行を前提としたものではなく、ハイブリッドシステムの動作を記述するための言語である。したがって、無限小を導入したプログラミング言語は、ハイブリッドシステムのモデリング言語ということができる。
【００３７】
［２．１ モデリング言語ｗｈｉｌｅｄｔの仕様］
以下に、本実施形態で用いられるｗｈｉｌｅｄｔ言語の定義の例を示す。
【数１】
【００３８】
ｗｈｉｌｅｄｔ言語の定義は、ＢＮＦ記法で記述されており、例えば、
ａ：：＝ｘ｜ｒ｜ｄｔ｜ａ１ ａｏｐ ａ２
は、「ａは、ｘ，ｒ，ｄｔもしくはａ１ ａｏｐ ａ２のいずれかである」という意味である。
ａは、算術式で、変数、実数定数、無限小を表す記号ｄｔか、算術演算（ａｏｐ）のいずれかである。
ｂは、真偽値を表す式で、真を表す値、偽を表す値、ブール演算（ａｎｄ演算、ｏｒ演算またはｎｏｔ演算）または算術式間の関係式（ａ１＜ａ２等）のいずれかである。
【００３９】
ｃはコマンド（プログラムで実行される文）であり、それぞれの意味は以下の
通りである。
ｓｋｉｐ ： なにも実行せずに終了する。
ｘ：＝ａ ： 算術式ａを評価し、その評価結果を変数ｘに代入する。
ｃ１；ｃ２ ： コマンドｃ１を実行し、その後コマンドｃ２を実行する。
ｉｆ ｂ ｔｈｅｎ ｃ１ ｅｌｓｅ ｃ２： 式ｂを評価し、その結果が真ならばｃ１を実行し、偽ならばｃ２を実行する。
ｗｈｉｌｅＱ ｂ ｄｏ ｃ ｄｏｎｅ ： 式ｂが真である間、ｃを繰り返し実行する。
【００４０】
上記のように、ｗｈｉｌｅｄｔ言語の定義では、算術式ａの定義に、無限小を示す記号ｄｔが導入されている。無限小を示す記号ｄｔに関する定義の部分を除くと、ｗｈｉｌｅｄｔ言語の定義は、一般的な手続き型プログラミング言語に準拠したものとなっている。
つまり、ｗｈｉｌｅｄｔ言語は、手続き型プログラミング言語を、無限小が記述できるように拡張した言語、ということができる。
なお、ｗｈｉｌｅｄｔ言語の定義は、上記のものに限られず、さらに拡張されていてもよい。本実施形態では、算術演算（ａｏｐ）に累乗を含めるなど、上記定義をさらに拡張したものを用いる。
【００４１】
［２．２ ｗｈｉｌｅｄｔ言語によるプログラム例（モデル例）］
［例１］
初めに非常にシンプルなｗｈｉｌｅｄｔのプログラム例を示す。このプログラムは微分方程式
【数２】
に従ったｘ(ｔ)の時間発展を時刻５まで計算する。ｗｈｉｌｅコマンドの各ループにおいて、ｘの値は微分方程式で指定された現時刻でのｘの微小変化量(ｘ×ｄｔ)だけ変化する。プログラム中のａｓｓｅｒｔ（ｘ≧２ａ）は、この時点においてｘ≧２ａが成り立たなければならないということを表しており、この条件が必ず成り立つことを、後述のプログラム論理を用いて検証する。
【００４２】
【数３】
【００４３】
［例２］
他の一例として先行研究（Ａｎｄｒｅ Ｐｌａｔｚｅｒ．Ｄｉｆｆｅｒｅｎｔｉａｌ ｄｙｎａｍｉｃ ｌｏｇｉｃ ｆｏｒ ｈｙｂｒｉｄ ｓｙｓｔｅｍｓ． Ｊ． Ａｕｔｏｍ．Ｒｅａｓｏｎｉｎｇ， ４１（２）:１４３-１８９， ２００８．）にて取り上げられているヨーロッパ鉄道制御システム（ＥＴＣＳ）のモデルを挙げる。
Ｃａｃｃｅｌは定数加速度ａで時刻εまで加速する電車をモデル化している。
ここで変数ｖは電車の速度、変数ｚは電車の位置を表現している。ｗｈｉｌｅループで時刻ｔを無限小量ずつ変化させ、コマンドＣｄｒｉｖｅ内ではｖ：＝ｖ＋ａ×ｄｔで速度ｖを、加速度ａに応じて変化させ、ｚ：=ｚ+ｖ×ｄｔで電車の位置ｚを現在の速度ｖに応じて変化させている。
【数４】
【００４４】
また、以下のプログラムｃｃｈｋＡｎｄＢｒａｋｅは、電車の位置を時間間隔εでモニタリングし、現在の位置が点ｍより距離ｓを越えていることを検知すると加速度を−ｂに変化させ減速し停車する電車をモデル化している。
【数５】
【００４５】
［例３］
別の現実に近い例として、先行研究（Ｒａｊｅｅｖ Ａｌｕｒ， Ｃｏｓｔａｓ Ｃｏｕｒｃｏｕｂｅｔｉｓ， Ｔｈｏｍａｓ Ａ． Ｈｅｎｚｉｎｇｅｒ， aｎｄ Ｐｅｉ−Ｈｓｉｎ Ｈｏ． Ｈｙｂｒｉｄ ａｕｔｏｍａｔａ： Ａｎ ａｌｇｏｒｉｔｈｍｉｃ ａｐｐｒｏａｃｈ ｔｏ ｔｈｅ ｓｐｅｃｉｆｉｃａｔｉｏｎ ａｎｄ ｖｅｒｉｆｉｃａｔｉｏｎ ｏｆ ｈｙｂｒｉｄ ｓｙｓｔｅｍｓ． Ｉｎ Ｈｙｂｒｉｄ Ｓｙｓｔｅｍｓ， ｐａｇｅｓ ２０９-２２９， １９９２．）にて取り上げられている貯水槽モニタのモデルを挙げる。
図２に示すように、この貯水槽１００には給水口１０１と排水口１０２が付いており、給水口１０１のバルブ１０３が開いているときは水位が毎秒１ｃｍで上昇し、バルブ１０３が閉じているときには毎秒２ｃｍで下降する。バルブ１０３の操作はスイッチ１０４で行われており、バルブ１０３の開閉はスイッチ１０４の操作後２秒経ってから起こる。
【００４６】
この貯水槽をモデル化したのが以下のプログラムｃｗａｔｅｒである。変数ｙは水位を、変数ｘはスイッチ操作からの変化時間を、ｓはスイッチの状態(１＝ｏｎ，０＝ｏｆｆ)を、ｖはバルブ１０３の状態（１＝開，０＝閉）を表している。
以下のプログラムにおいて、ｃａｓｅ｛・・・｝は、初めから順番に条件を検査し、条件が成り立った部分のプログラムを実行する構文である。
【数６】
【００４７】
［３．検証装置（プログラム論理を用いた検証アルゴリズム）］
ｗｈｉｌｅｄｔ言語によってコーディングされたハイブリッドシステムのモデルは、プログラミング言語的に記述されているため、形式的検証を行うプログラム検証器４５によって検証が可能である。
【００４８】
図１に示すように、検証装置４は、ｗｈｉｌｅｄｔ言語によってコーディングされたハイブリッドシステムのモデルのコード（プログラム）の入力を受け付ける入力部４１を備えている。入力部４１は、システム１内部の他の機能（例えば、図１の変換器３）から、コードの入力を受け付けても良いし、システム１の外部からコードの入力を受け付けても良い。
【００４９】
モデルのコード等の入力部４１によって受け付けたデータは、記憶部４２によって記憶される。記憶部４２に記憶されたコード等に対して、検証の前処理を行う処理部（セクション化部４３、ループ不変表明計算部４４）が、所定の前処理を行い、その前処理の結果を、再び、記憶部４２に記憶させる。
【００５０】
また、プログラム検証器４５は、記憶部４２に記憶されたコード（必要に応じて前処理の施された後のコード）に対して、形式的検証によって検証を行う。プログラム検証器４５は、検証条件を生成するための検証条件生成器４６と、検証条件として生成された論理式を証明する定理証明器４７と、を有している。
さらに、検証装置４は、定理証明器４７による証明結果（検証結果）を、ハイブリッドシステムの検証結果として出力するための出力部４８を備えている。
【００５１】
検証装置４の入力部４１は、検証対象のプログラムのコード（ハイブリッドシステムの動作をｗｈｉｌｅｄｔ言語でコーディングしたコード）ｃと、当該プログラムの実行前に必ず成り立っているべき条件(事前条件)Ｑと、を入力として受け取る。事前条件Ｑは、ハイブリッドシステムの品質を保証するための品質保証条件となる論理式である。なお、品質保証条件は、プログラムの実行後に必ず成り立っているべき条件（事後条件）など、他の条件であってもよい。
【００５２】
コードｃ中には、ａｓｓｅｒｔ（Ｑ’）（ただし、Ｑ’は、プログラム変数に関する論理式）という文が各所に記述されている。検証装置４の出力部４８は、与えられた事前条件Ｑが成り立つ状態でプログラムがモデル化しているハイブリッドシステムの実行を開始したと考えた場合に、プログラムｃ中のａｓｓｅｒｔ（Ｑ’）で示された論理式が必ず成り立つならば「検証成功」、成り立たない場合があるならば「検証失敗」を、出力する。
【００５３】
検証装置４による検証アルゴリズムにおける具体的な手続きは以下の通りである。
１）プログラムｃ、事前条件Ｑについてセクション化の操作を行う（置換ステップ）。
２）セクション化後のプログラムｃについて、ループ不変表明の計算の操作を行う（付加ステップ）。
３）プログラムｃについて検証条件（論理式）の生成を行う（検証ステップ）。
４）検証条件が成り立つことを、定理証明器を用いて証明する。この証明に定理証明器が成功した場合は検証成功、成功しなかった場合は検証失敗を返す（検証ステップ）。
【００５４】
上記のアルゴリズムで検証を行うと、プログラムが与えられた性質を必ず満たすことが数学的に保証される。これにより、ハイブリッドシステムの品質に数学的な保証を与えることができ、ハイブリッドシステムの品質を大きく向上させることが可能となる。
【００５５】
以下、検証アルゴリズムの動作について説明する。以下では、説明の簡略化のため、例１のプログラム例についてアルゴリズムの動作を説明するが、例２、例３のプログラムについてもこのアルゴリズムが正しく動くことは確認済みである。
【００５６】
［３．１ プログラムｃと事前条件Ｑのセクション化］
前記置換ステップでは、セクション化部（置換処理部）４３が、入力として与えられたプログラムｃと事前条件Ｑについてセクション化という操作を行う。セクション化とは、無限小を示す表現であるｄｔを、実数値を示す表現”１／ｉ”に置換する操作である。実数値を示す表現”１／ｉ”は、数値を示す記号”ｉ”を含んでおり、ｉが示す値（の絶対値）が増加したと考えた場合、その増加につれて、表現”１／ｉ”が示す値が０に収束する値を示す表現となっている。つまり、ｉの絶対値が非常に大きくなれば、１／ｉは０に収束する。ここでは、ｉは、正の整数であるとするが、負の整数であってもよい。また、実数値を示す値は、”１／ｉ”に限らず、例えば、”１／（２×ｉ）”または”１／（３×ｉ）”などであってもよい。セクション化の操作によりｗｈｉｌｅｄｔのプログラムｃと事前条件Ｑとが、(無限小の値を含まない)実数上のプログラムｃｉ・論理式Ｑｉに変換される。セクション化により、無限小値を含むプログラムの検証に無限小値を対象としない既存手法（例えば、以下で述べるループ不変表明の計算等）を適用することが可能となる。
【００５７】
例として、前記プログラム例１について、
【数７】
のもとでの検証例を見る。
【００５８】
この例について、セクション化（置換ステップ）の結果得られるプログラムｃｉと論理式Ｑｉは、次のようになる。
【数８】
【００５９】
［３．２ ループ不変表明の計算］
前記付加ステップでは、ループ不変表明計算部４４が、セクション化して得られたプログラムｃｉについてループ不変表明（ｌｏｏｐ ｉｎｖａｒｉａｎｔ ａｓｓｅｒｔｉｏｎ）を計算し、プログラムｃｉに付加する。
【００６０】
ループ不変表明とは、プログラム中のループが、要求される仕様を満たしているか否かを検証するための論理式である。ループ不変表明は、セクション化されたプログラムｃｉ中のループ文において、ループの入口と出口で必ず成り立っているべき論理式として記述される。ループ不変表明計算部４４は、ループ不変表明を構成する論理式を、自動的に生成して、プログラムｃｉ中に付加する。
ループ不変表明を自動生成するアルゴリズムとしては、例えば、Ｓｒｉｒａｍ Ｓａｎｋａｒａｎａｒａｙａｎａｎ、 Ｈｅｎｎｙ Ｂ． Ｓｉｐｍａ， ａｎｄ Ｚｏｈａｒ Ｍａｎｎａ． Ｎｏｎｌｉｎｅａｒ ｌｏｏｐ ｉｎｖａｒｉａｎｔ ｇｅｎｅｒａｔｉｏｎ ｕｓｉｎｇ ｇｒｏｅｂｎｅｒ ｂａｓｅｓ． Ｉｎ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ３１ｓｔ ＡＣＭ ＳＩＧＰＬＡＮ−ＳＩＧＡＣＴ ｓｙｍｐｏｓｉｕｍ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ｏｆ ｐｒｏｇｒａｍｍｉｎｇ ｌａｎｇｕａｇｅｓ， ＰＯＰＬ ’０４， ｐａｇｅｓ ３１８-３２９， Ｎｅｗ Ｙｏｒｋ， ＮＹ， ＵＳＡ，２００４． ＡＣＭ．に開示されているものを利用することができる。ループ不変表明の計算・付加は、手動で行っても良い。
【００６１】
また、ループ不変表明の計算は、プログラムｃｉに、ｗｈｉｌｅ文などのループ文が含まれている場合には、行う必要があるが、ループ文が含まれていない場合は、行う必要がない。
【００６２】
例として、前節のセクション化されたプログラムｃｉについてはループ不変表明として
【数９】
をとることができる。
【００６３】
すなわち、ループの入口と出口において、必ずｔ＝ｎ／ｉとｘ＝（１＋１／ｉ）ｎが成り立つような０以上のｎが存在する。実際に、ｃｉ中のｗｈｉｌｅ文においては初めてループに入る時にはｘ＝１かつｔ＝０が成り立っているので、ｎとして０を取ればループ不変表明は成り立つ。また、ループの入口でループ不変表明が成り立っているときにループ本体を一回実行すると、ｔの値は１／ｉだけ増加し、ｘの値は、（１＋１／ｉ）倍されるので、上記の論理式のｎをｎ＋１と取り直せば、やはりループの出口でもループ不変表明が成り立っている。
【００６４】
［３．３ 検証条件の生成］
プログラム検証器４５の検証条件生成器４６は、記憶部４２に記憶されたプログラム（セクション化され、ループ不変表明が付加されたプログラム）ｃｉ、及び事前条件（セクション化された事前条件）Ｑｉについて、検証条件の生成という手続きを行う。
【００６５】
検証条件とは、記述した性質が確かに成り立つための十分条件である。すなわち、生成された検証条件とＱｉが成り立つ状況下でｃｉを実行すると必ずＱｉ’が成り立つ。
【００６６】
検証条件生成器４６における検証条件生成アルゴリズムは、プログラム論理と呼ばれる手法に基づいて設計されている。
【００６７】
以下に、プログラム論理に基づく検証条件生成アルゴリズムＶＣを示す。
【数１０】
【００６８】
検証条件生成アルゴリズムＶＣでは、プログラムｃ（セクション化され、ループ不変表明が付加されたプログラム）と、事前条件Ｑを受け取り、検証条件を生成する。
アルゴリズムＶＣは、再帰関数ＶＣ１を用いて定義されている。
ＶＣ１（ｃ，Ｑ）は、プログラムｃの実行後に、Ｑが成り立つために、ｃの実行前に成り立っているべき条件を返す。
例えば、ＶＣ１（ｃ１；ｃ２，Ｑ）の定義は、「ＶＣ１（ｃ２，Ｑ）の結果をＱ’’、ＶＣ１（ｃ１，Ｑ’’）の結果をＱ’としたときに、全体の結果はＱ’である」のように読む。
ＶＣは、「ＶＣ１によって返された条件が、事前条件から帰結される」ことを意味する論理式を検証条件として返す。
なお、検証条件生成アルゴリズムにおいて、Ｑ［ｘ−＞ａ］は、Ｑ中の変数ｘをａで置き換える操作を示す。
【００６９】
プログラム論理に基づく検証条件生成アルゴリズムでは、プログラム全体の検証条件が、その部分プログラムの検証条件の組み合わせで計算されている。これにより、巨大なシステム全体の性質を検証する際に、その構成要素の性質を用いて計算することが容易になる。
【００７０】
例１のプログラムについて検証条件生成アルゴリズムＶＣを適用すると、検証条件として以下の論理式が生成される。
【数１１】
なお、Ｑ’’（ｔ，ｘ，ｉ）は、ループ不変表明計算部４４によって計算されたループ不変表明である。
【００７１】
［３．４ 定理証明器を用いた検証条件の証明］
前述のように生成された検証条件が、「有限個のｉを除いて正しい」ことが示されれば、元のｗｈｉｌｅｄｔのプログラムｃは、与えられた性質を必ず満たす。この検証条件（論理式）の証明のため、本実施形態では、定理証明器（Ｔｈｅｏｒｅｍ Ｐｒｏｖｅｒ）４７を用いる。プログラム検証の分野においては、与えられた論理式が成り立つかどうかを自動的に判定する手法（Ｂｅｈｅａｄｓ Ａｋｂａｒｐｏｕｒ ａｎｄ Ｌ． Ｃ． Ｐａｕｌｓｏｎ． Ｍｅｔｉｔａｒｓｋｉ： Ａｎ ａｕｔｏｍａｔｉｃ ｔｈｅｏｒｅｍ ｐｒｏｖｅｒ ｆｏｒ ｒｅａｌ−ｖａｌｕｅｄ ｓｐｅｃｉａｌ ｆｕｎｃｔｉｏｎｓ． Ｊ． Ａｕｔｏｍａｔｅｄ Ｒｅａｓｏｎｉｎｇ，４４（３）：１７５-２０５， ２０１０．）や、一部人間の支援によって判定する手法（Ｔｈｅ Ｃｏｑ Ｄｅｖｅｌｏｐｍｅｎｔ Ｔｅａｍ． Ｒｅｆｅｒｅｎｃｅ Ｍａｎｕａｌ - Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ．ＩＮＲＩＡ， ２０１０． ｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ／ｒｅｆａｎ／．）が知られており、これらの手法を用いて検証条件が成り立つかどうかを判定する。
【００７２】
生成された検証条件をＱｉとすると、前述の「有限個のｉを除いてＱｉが成り立つ」という条件は、論理式を用いて、
【数１２】
と書ける。
【００７３】
したがって、この論理式を定理証明器で証明することによって、元のプログラム中のａｓｓｅｒｔ（Ｑ）が必ず成り立つことが検証できる。
例１のプログラムについての検証条件を整理すると、
【数１３】
が成り立てば、検証条件が成り立つことが分かる。
したがって、定理証明器４７で証明すべき論理式は、
【数１４】
となる。この論理式が成り立つことは、定理証明器４７を用いて証明することが可能である。
【００７４】
［３．５ セクション化について］
上記のアルゴリズムＶＣに先立ちセクション化という操作を行っている。この操作は無限小値を含むプログラムの検証を、実数のみを扱える定理証明器を用いて行うために必要な操作である。本実施形態では、プログラムｃのセクション化を行ってから以降の手続きを行っているが、プログラムｃのセクション化を行わずにループ不変表明の計算と検証条件の生成を行い、その後、検証条件をセクション化して、定理証明器４７に渡しても良い。
【００７５】
また、無限小値を直接扱うことのできる定理証明器を用いることが可能な場合は、セクション化を行うことなく検証条件の生成と定理証明器での証明を行うことが可能である。
また、セクション化の手法は、プログラム論理を用いない他の検証手法をｗｈｉｌｅｄｔで記述されたプログラムの検証を行う場合にも有効である。
【００７６】
［４．検証例］
［４．１ ｗｈｉｌｅｄｔのプログラムの例Ａ］
ｗｈｉｌｅｄｔによってハイブリッドシステムの動作をコーディングしたモデルのプログラムコードＡを、以下に示す。なお、以下のコードにおいて、「＆＆」は、論理積を示す論理演算子である。
【数１５】
【００７７】
［４．２ セクション化］
例Ａのコードをセクション化したコードＡ１を、以下に示す。セクション化により、例Ａのコードに含まれていたｄｔ（無限小を表す記号）が、”１／ｉ”に変換され、無限小ｄｔを含まない形となっている。したがって、既存のソフトウェア検証手法を適用することが可能となっている。
【数１６】
【００７８】
［４．３ ループ不変表明の付加］
セクション化されたコードＡ１に、ループ不変表明を付加したコードＡ２を、以下に示す。
【数１７】
【００７９】
［４．４ 検証条件］
セクション化され、かつ、ループ不変表面が付加されたコードＡ２に対し、事前条件をｔｒｕｅとして、検証条件生成アルゴリズムＶＣを適用して得られる検証条件を、以下に示す。この検証条件は、定理証明器Ｃｏｑ（ｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ／ｒｅｆａｎ／）で扱えるフォーマットで記述されている。なお、実際に定理証明器で証明すべき論理式は、以下に示す論理式の先頭に、「ｅｘｉｓｔｓ ｎ：ｎａｔ，ｉ＞ｎ −＞」を付加したものになる。
【数１８】
【００８０】
［４．５ セクション化せずにループ不変表明を付加］
例ＡのコードＡを、セクション化せずにループ不変表明を付加したコードＡ３を、以下に示す。
【数１９】
【００８１】
［４．６ セクション化せずに生成された検証条件］
セクション化せずにループ不変表明を付加したコードＡ３に対し、事前条件をｔｒｕｅとして、検証条件生成アルゴリズムＶＣを適用して得られる検証条件を、以下に示す。
無限小を直接扱える定理証明器を用いれば、この検証条件の証明を行うことで、コードＡの安全性を示すことができる。無限小を扱える定理証明器としては、（Ｔａｎｉａ Ｂｅｄｒａｘ−Ｗｅｉｓｓ ａｎｄ Ｒｏｌａｎｄｏ Ｃｈｕａｑｕｉ， ＩＮＦＭＡＬ： Ａｎ Ｉｎｆｉｎｉｔｅｓｉｍａｌ Ａｎａｌｙｓｉｓ Ｉｎｔｅｒａｃｔｉｖｅ Ｔｈｅｏｒｅｍ Ｐｒｏｖｅｒ ａｎｄ Ｐｒｏｂｌｅｍ Ｓｏｌｖｅｒ． Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ＸＩＩ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｆ ｔｈｅ Ｃｈｉｌｅａｎ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ Ｓｏｃｉｅｔｙ， Ｓａｎｔｉａｇｏ， Ｃｈｉｌｅ， Ｏｃｔｏｂｅｒ １９９２．）に記載のものがある。以下の検証条件中のｄｔを”１／ｉ”で置き換えたものは、［４．４ 検証条件］で示した検証条件と一致する。
【数２０】
【００８２】
［５．ｗｈｉｌｅｄｔプログラムへの変換］
図３は、図１に示す変換装置３におけるモデル変換処理を示している。図１に示すように、変換装置３は、生成部３ａと、変換テーブル３ｂと、を備えている。
生成部３ａは、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図（モデル）から、ｗｈｉｌｅｄｔ言語でコーディングされたプログラム（ハイブリッドシステムのモデルのコード）を生成する。
変換テーブル３ｂは、ハイブリッドシステムのブロック線図から、ｗｈｉｌｅｄｔ言語のプログラムコードに生成するために、生成部３ａによって参照される。
【００８３】
変換装置３は、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図のデータの入力を受け付けると（ステップＳ１）、コードの生成を開始する。
【００８４】
図４は、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図の例を示している。このブロック線図は、時刻１で値が０から１になるステップ信号を生成して出力するブロック５１、入力信号の加減算を行って出力するブロック５２、入力信号を増幅して出力するブロック５３ａ，５３ｂ，５３ｃ、入力信号の積分をして出力するブロック５４ａ，５４ｂ等の各種ブロックを備えている。各ブロックは、結線Ｌ１〜Ｌ７によって適宜接続されている。
【００８５】
コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図のデータには、ブロック線図中のブロック及び結線を示すデータの他、各ブロックに設定されたパラメータ（例えば、入力信号を増幅して出力するブロック５３ａ，５３ｂ，５３ｃであれば、ゲイン値）を示すデータが含まれている。
【００８６】
変換装置３の生成部３ａは、ブロック線図のデータに基づいて、ブロック線図中の各結線Ｌ１〜Ｌ７に対応する変数ｘｉ，ｘｉ’（ｉは、自然数）を生成する（ステップＳ２）。なお、途中で分岐する結線は、１本の結線であるとみなす。ここでは、各結線に対して、ｘｉ，ｘｉ’という２つの変数を生成する。
また、生成部３ａは、ブロック線図中の各ブロック５１，５２，５３ａ，５３ｂ，５３ｃ，５４ａ，５４ｂのうち、内部状態を持つブロック５４ａ，５４ｂについて、状態変数ｓｉ，ｓｉ’（ｉは、自然数）を生成する（ステップＳ３）。なお、積分ブロック５４ａ，５４ｂの場合、内部状態を示す値は、積分値である。状態変数についても、各ブロックに対してｓｉ，ｓｉ’という２つの変数が生成される。
図５は、図４のブロック線図に対して、変数生成処理（ステップＳ２，Ｓ３）を行って生成された変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’を示している。
【００８７】
さらに、生成部３ａは、時間を表す変数ｔを生成する（ステップＳ４）。
続いて、生成部３ａは、ステップＳ２〜４で生成した各変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’，ｔを初期化するコードｃ０を生成する（ステップＳ５）。以下は、各変数を０で初期化したコードｃ０の例を示している。
【数２１】
【００８８】
なお、ブロックに設定されたパラメータ（ブロック線図のデータ中のパラメータ）として、状態変数の初期値が設定されている場合には、設定された初期値が、生成された変数の初期値となるコードｃ０が生成される。
【００８９】
さらに続けて、生成部３ａは、無限小時間後の各変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’の値を計算して変数を更新するためのコードｃ１を生成する（ステップＳ６）。コードｃ１は、コードｃ１１と、コードｃ１２とからなる。
【００９０】
コードｃ１１は、各ブロックにおける無限小時間後の出力値として、変数ｘｉに基づいて計算される値を、ｘｉ’に代入するコードである（ここでは、ｘｉのｉと、ｘｉ’のｉとは、一般には異なる値である）。
生成部３ａは、ブロック線図中の各ブロックについて、変換テーブル３ｂを参照することで、コードｃ１１を生成する（ステップＳ６ａ）。なお、変換テーブル３ｂは、変換装置３を構成するコンピュータ又はその他の装置の記憶部に記憶されている。
【００９１】
図６は、ブロック線図において用いられるブロックと、ブロックに対応するｗｈｉｌｅｄｔ言語のコードとの対応を規定した変換テーブルの例を示している。なお、図６では、ブロック線図に用いられるブロックとして、Ｓｉｍｕｌｉｎｋで用いられるブロックの一部を例として挙げた。
図６の変換テーブル３ｂの左側が、Ｓｉｍｕｌｉｎｋにおいて用いられるブロックを示しており、変換テーブル３ｂの右側が、各ブロックに対応するｗｈｉｌｅｄｔ言語のコードを示している。
【００９２】
生成部３ａが、コードｃ１１を生成する際には、変換テーブル３ｂ中のｗｈｉｌｅｄｔ言語のコードにおける変数を示す記号のうち、ｘｉ，ｘｉ’，ｘｊは、変換対象のブロックの入力又は出力に接続された結線に割り当てられた変数名に置換される。また、変換テーブル３ｂ中のｗｈｉｌｅｄｔ言語のコードにおける変数を示す記号のうち、ｓｉ，ｓｉ’は、置換対象のブロックに割り当てられた状態変数名に置換される。
また、変換テーブル３ｂ中のｗｈｉｌｅｄｔ言語のコードにおけるその他の変数を示す記号（ｄｔを除く）は、置換対象のブロックに設定されたパラメータ（ブロック線図のデータ中のパラメータ）が示す値に置換される。
【００９３】
生成部３ａが、図５に示すブロック線図に関して、変換テーブル３ｂを参照することで生成したコードｃ１１を以下に示す。
【数２２】
【００９４】
コードｃ１２は、ｘｉ’，ｓｉ’の値を、ｘｉ，ｓｉに代入するコードである（ここでは、ｘｉのｉと、ｘｉ’のｉとは同じ値であり、ｓｉのｉと、ｓｉ’のｉも同じ値である）。
生成部３ａが、図５に示すブロック線図に関して、ｘｉ’，ｓｉ’の値を、ｘｉ，ｓｉに代入するコードとして生成したコードｃ１２を以下に示す。
【数２３】
【００９５】
さらに、生成部３ａは、無限小を示す記号ｄｔを用いて、時間を示す変数ｔを更新するコード（ｗｈｉｌｅ文）を生成し、先に生成したコードｃ０及びコードｃ１を組み合わせて、図５に示すハイブリッドシステムのブロック線図全体の動作を示すコード［ｃ０； ｗｈｉｌｅ （ｔ＜１／ｄｔ） ｛ｃ１；ｔ：＝ｔ＋ｄｔ｝］を生成する。
【００９６】
生成されたコードは、［ｃ０； ｗｈｉｌｅ （ｔ＜１／ｄｔ） ｛ｃ１；ｔ：＝ｔ＋ｄｔ｝］は、コンピュータの記憶部に記憶されて、検証装置４による検証に用いても良いし、表示装置などに出力されてもよい。
【００９７】
なお、変換装置３は、上述の変換処理とは逆の変換を行うことで、ブロック線図によって記述可能なハイブリッドシステムの動作を示すｗｈｉｌｅｄｔ言語のコードを、ブロック線図に変換することもできる。
【００９８】
なお、本実施形態では、ｗｈｉｌｅｄｔ言語のコードを、変換装置によって自動的に作成したが、人手でコーディングを行っても良い。
さらに、本実施形態では、ハイブリッドシステムの開発者として、ソフトウェア技術者を活用することが可能である。
すなわち、ハイブリッドシステムの開発現場では、制御理論に由来する開発手法が主に採用されているため、通常のソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが困難であった。しかし、本実施形態では、ハイブリッドシステムのモデルを、プログラミング言語によってコーディングできるため、プログラミング言語に慣れているソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが可能である。
【００９９】
［６．付記］
なお、上記において開示した事項は、例示であって、本発明を限定するものではなく、様々な変形が可能である。
【符号の説明】
【０１００】
１ システム
２ コンピュータ支援設計システム
３ 変換装置
３ａ 生成部
３ｂ 変換テーブル
４ 検証装置
４１ 入力部
４２ 記憶部
４３ セクション化部（置換処理部）
４４ ループ不変表明計算部
４５ プログラム検証器
４６ 検証条件生成器
４７ 定理証明器
４８ 出力部
【技術分野】
【０００１】
本発明は、ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラムに関するものである。
【背景技術】
【０００２】
ハイブリッドシステムは、制御理論における用語であり、速度や温度のような物理量を表す連続値と、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値とが相互に影響を及ぼしあってシステム全体が動作するのが特徴である。
【０００３】
典型的なハイブリッドシステムとしては、自動車や航空機など、物理量の制御にソフトウェアが関わるようなシステムが挙げられる。例えば、自動車においては、モータの回転数、ブレーキオイルの圧力、内燃機関での燃焼量といった連続値と、ＡＢＳを動作させるかどうか等の離散値とが、時々刻々と変化しながら自動車の動作を実現している。
このため、ハイブリッドシステムは、連続値のみを扱うプラントや離散値のみを扱うソフトウェアとは異なった複雑さを持っている。
【０００４】
ハイブリッドシステムを記述できるシステムとして、ＭａｔｈＷｏｒｋｓ社のＳｉｍｕｌｉｎｋなどがある。
連続的な値のみを扱うシステムを対象とする従来の制御理論では、信号の流れを、図式を用いて表現する手法がよく用いられる。これを計算機上に実現し、さらに離散的な状態変化を表現するブロックを追加して拡張したのが、Ｓｉｍｕｌｉｎｋなどの枠組みである。
【０００５】
現在、ハイブリッドシステムの開発現場では、Ｓｉｍｕｌｉｎｋなどの枠組みを利用して、ハイブリッドシステムの開発が行われている。
【先行技術文献】
【非特許文献】
【０００６】
【非特許文献１】インターネット＜ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｍａｔｈｗｏｒｋｓ．ｃｏｍ／ｐｒｏｄｕｃｔｓ／ｓｉｍｕｌｉｎｋ/＞
【発明の概要】
【発明が解決しようとする課題】
【０００７】
ここで、ハイブリッドシステムが意図した通りに動作することを検証することは非常に重要な問題である。
一般に、システムが意図した通りに振る舞うことを検証するために、シミュレーションによるテストがよく用いられる。これは、様々な入力をシステムに繰り返し与え、その動作が意図した通りであることを確認することで、システムの品質を担保しようとする手法である。
【０００８】
例えば、Ｓｉｍｕｌｉｎｋを用いてハイブリッドシステムの開発を行う場合には、Ｓｉｍｕｌｉｎｋ上で図式によって表現されたハイブリッドシステムに対して、いろいろな信号を入力として与えて、そのハイブリッドシステムの振る舞いをＳｉｍｕｌｉｎｋ上で確認することで、ハイブリッドシステムの品質をチェックすることができる。
【０００９】
しかしながら、シミュレーションによるテストに基づく品質チェックのみでは 、全ての入力を網羅することが不可能である。したがって、シミュレーションの際に用いなかった入力に対しての品質の担保が全く無い。
【００１０】
そこで、本発明は、ハイブリッドシステムの検証のための新たな技術的手段を提供することを目的とする。
【課題を解決するための手段】
【００１１】
（１）本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされている
ハイブリッドシステムの検証方法である。
【００１２】
（２）前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。
【００１３】
（３）前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証するのが好ましい。
【００１４】
（４）前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。
【００１５】
（５）前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。
【００１６】
（６）前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含むのが好ましい。
【００１７】
（７）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備えているハイブリッドシステムの検証装置である。
【００１８】
（８）前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。
【００１９】
（９）前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現形式に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証するのが好ましい。
【００２０】
（１０）前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。
【００２１】
（１１）前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。
【００２２】
（１２）前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備えるのが好ましい。
【００２３】
（１３）他の観点からみた本発明は、コンピュータを、前記（７）〜（１２）のいずれか１項に記載の検証装置として機能させるためのコンピュータプログラムである。
【００２４】
（１４）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法である。
（１５）他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置である。
（１６）他の観点からみた本発明は、コンピュータを、前記（１５）のモデル変換装置として機能させるためのコンピュータプログラムである。
【図面の簡単な説明】
【００２５】
【図１】ハイブリッドシステムの設計支援及び検証のためのシステムの構成図である。
【図２】貯水槽のモデルを示す図である。
【図３】モデル変換処理のフローチャートである。
【図４】コンピュータ設計支援システムによって作成されたハイブリッドシステムのブロック線図である。
【図５】ブロック線図の結線及びブロックに付与された変数を示す図である。
【図６】変換テーブルを示す図である。
【発明を実施するための形態】
【００２６】
以下、本発明の好ましい実施形態について添付図面を参照しながら説明する。
【００２７】
［１．ハイブリッドシステムの設計支援及び検証のためのシステム］
図１は、ハイブリッドシステムの設計支援及び検証のためのシステム１を示している。このシステム１は、ハイブリッドシステムの作成を行うことができるコンピュータ支援設計システム２と、コンピュータ支援設計システム２で作成したハイブリッドシステムを、ハイブリッドシステムをモデル化したプログラムに変換する変換器と、プログラミング言語によってコーディングされたハイブリッドシステムを検証する検証装置４と、を備えている。
【００２８】
なお、システム１の各機能は、コンピュータの記憶装置にインストールされたコンピュータプログラムが、コンピュータに実行されることによって発揮される。そのコンピュータプログラムは、記録媒体に記録して、譲渡・販売することができる。
【００２９】
本実施形態では、ハイブリッドシステムを検証するために、コンピュータ支援設計システム２で作成したハイブリッドシステムに対して、様々な入力を与えてシミュレーションを行うのではなく、プログラムに対する形式的検証を用いて検証を行う。
ここで、プログラム（ソフトウェア）の開発においては、形式的検証（形式的手法によるプログラム検証）による検証が用いられつつある。形式的検証とは、数理科学的に正しさが証明されたアルゴリズム（例えば、定理証明器）で、プログラムを解析し、プログラムにバグが無いことを保証する手法である。なお、形式的検証については、例えば、「林 晋、プログラム検証論 (情報数学講座) 、共立出版、１９９４」に開示されている。
形式的検証では、様々な入力を与えてテストすることなく、すべての入力について網羅的にテストを行ったのと同じ結果が得られる。
【００３０】
様々な入力を与えてテストすることで検証を行う方法では、システムをモジュール化した場合に、モジュール毎の品質保証ができたとしても、モジュールを組み合わせたシステム全体の品質保証が困難である。しかし、形式的検証には、モジュール毎の品質保証によって、モジュールを組み合わせたシステム全体の品質保証が可能な技術が多く存在するので、モジュール性を確保することが容易である。
【００３１】
このように、形式的検証は、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易である。
このように優れた特性を持つ形式的検証の手法を、ハイブリッドシステムの検証に利用するという点が、本発明者らの着想の第一点である。
【００３２】
そして、本発明者らの着想の第二点は、プログラミング言語を、ハイブリッドシステムの動作の記述に用いることである。
プログラミング言語は、元来、コンピュータによって実行されるプログラムコードを記述するためのものであり、ハイブリッドシステムの動作を記述するものではない。
従来のプログラミング言語であっても、ハイブリッドシステムの動作のうち、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値の変化は、当然に、記述できる。
【００３３】
しかし、ハイブリッドシステムの動作には、ソフトウェアによって制御されるがソフトウェアの動作そのものではない連続値（速度や温度のような物理量）の変化も含まれる。従来、ソフトウェアの動作ではない連続値の変化そのものは、プログラミング言語による記述の対象になっていない。
【００３４】
これに対して、本実施形態のシステム１では、ハイブリッドシステムの記述のために拡張されたプログラミング言語が用いられる。その拡張されたプログラミング言語（モデリング言語）によって、連続値の変化を含むハイブリッドシステムの動作が、モデリングされる。そして、拡張されたプログラミング言語を用いてモデリングされたハイブリッドシステムを、プログラム検証技術である形式的検証の手法によって検証する。
これにより、ハイブリッドシステムを、プログラムの検証と同様の手法で検証でき、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易となる。
【００３５】
［２． ハイブリッドシステムのモデリング言語］
本実施形態では、手続き型プログラミング言語のエッセンスであるｗｈｉｌｅ言語（Ｇｌｙｎｎ Ｗｉｎｓｋｅｌ． Ｆｏｒｍａｌ Ｓｅｍａｎｔｉｃｓ ｏｆ Ｐｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ． Ｔｈｅ ＭＩＴ Ｐｒｅｓｓ， Ｆｅｂｒｕａｒｙ １９９３．）を、無限小の値を表すｄｔという記号で拡張した言語であるｗｈｉｌｅｄｔを用いる。
無限小の値を言語に加えることにより、連続量を扱うシステムを、手続き型プログラミング言語で記述することができる。
【００３６】
つまり、プログラミング言語は、元来、ソフトウェアの動作に関わる離散値を記述できるものであるから、無限小の導入によって連続値が記述可能となれば、連続値と離散値とが相互に影響を及ぼしあって変化するハイブリッドシステムの動作が記述可能となる。
なお、無限小を導入したプログラミング言語（ｗｈｉｌｅｄｔ言語）は、コンピュータによる実行を前提としたものではなく、ハイブリッドシステムの動作を記述するための言語である。したがって、無限小を導入したプログラミング言語は、ハイブリッドシステムのモデリング言語ということができる。
【００３７】
［２．１ モデリング言語ｗｈｉｌｅｄｔの仕様］
以下に、本実施形態で用いられるｗｈｉｌｅｄｔ言語の定義の例を示す。
【数１】
【００３８】
ｗｈｉｌｅｄｔ言語の定義は、ＢＮＦ記法で記述されており、例えば、
ａ：：＝ｘ｜ｒ｜ｄｔ｜ａ１ ａｏｐ ａ２
は、「ａは、ｘ，ｒ，ｄｔもしくはａ１ ａｏｐ ａ２のいずれかである」という意味である。
ａは、算術式で、変数、実数定数、無限小を表す記号ｄｔか、算術演算（ａｏｐ）のいずれかである。
ｂは、真偽値を表す式で、真を表す値、偽を表す値、ブール演算（ａｎｄ演算、ｏｒ演算またはｎｏｔ演算）または算術式間の関係式（ａ１＜ａ２等）のいずれかである。
【００３９】
ｃはコマンド（プログラムで実行される文）であり、それぞれの意味は以下の
通りである。
ｓｋｉｐ ： なにも実行せずに終了する。
ｘ：＝ａ ： 算術式ａを評価し、その評価結果を変数ｘに代入する。
ｃ１；ｃ２ ： コマンドｃ１を実行し、その後コマンドｃ２を実行する。
ｉｆ ｂ ｔｈｅｎ ｃ１ ｅｌｓｅ ｃ２： 式ｂを評価し、その結果が真ならばｃ１を実行し、偽ならばｃ２を実行する。
ｗｈｉｌｅＱ ｂ ｄｏ ｃ ｄｏｎｅ ： 式ｂが真である間、ｃを繰り返し実行する。
【００４０】
上記のように、ｗｈｉｌｅｄｔ言語の定義では、算術式ａの定義に、無限小を示す記号ｄｔが導入されている。無限小を示す記号ｄｔに関する定義の部分を除くと、ｗｈｉｌｅｄｔ言語の定義は、一般的な手続き型プログラミング言語に準拠したものとなっている。
つまり、ｗｈｉｌｅｄｔ言語は、手続き型プログラミング言語を、無限小が記述できるように拡張した言語、ということができる。
なお、ｗｈｉｌｅｄｔ言語の定義は、上記のものに限られず、さらに拡張されていてもよい。本実施形態では、算術演算（ａｏｐ）に累乗を含めるなど、上記定義をさらに拡張したものを用いる。
【００４１】
［２．２ ｗｈｉｌｅｄｔ言語によるプログラム例（モデル例）］
［例１］
初めに非常にシンプルなｗｈｉｌｅｄｔのプログラム例を示す。このプログラムは微分方程式
【数２】
に従ったｘ(ｔ)の時間発展を時刻５まで計算する。ｗｈｉｌｅコマンドの各ループにおいて、ｘの値は微分方程式で指定された現時刻でのｘの微小変化量(ｘ×ｄｔ)だけ変化する。プログラム中のａｓｓｅｒｔ（ｘ≧２ａ）は、この時点においてｘ≧２ａが成り立たなければならないということを表しており、この条件が必ず成り立つことを、後述のプログラム論理を用いて検証する。
【００４２】
【数３】
【００４３】
［例２］
他の一例として先行研究（Ａｎｄｒｅ Ｐｌａｔｚｅｒ．Ｄｉｆｆｅｒｅｎｔｉａｌ ｄｙｎａｍｉｃ ｌｏｇｉｃ ｆｏｒ ｈｙｂｒｉｄ ｓｙｓｔｅｍｓ． Ｊ． Ａｕｔｏｍ．Ｒｅａｓｏｎｉｎｇ， ４１（２）:１４３-１８９， ２００８．）にて取り上げられているヨーロッパ鉄道制御システム（ＥＴＣＳ）のモデルを挙げる。
Ｃａｃｃｅｌは定数加速度ａで時刻εまで加速する電車をモデル化している。
ここで変数ｖは電車の速度、変数ｚは電車の位置を表現している。ｗｈｉｌｅループで時刻ｔを無限小量ずつ変化させ、コマンドＣｄｒｉｖｅ内ではｖ：＝ｖ＋ａ×ｄｔで速度ｖを、加速度ａに応じて変化させ、ｚ：=ｚ+ｖ×ｄｔで電車の位置ｚを現在の速度ｖに応じて変化させている。
【数４】
【００４４】
また、以下のプログラムｃｃｈｋＡｎｄＢｒａｋｅは、電車の位置を時間間隔εでモニタリングし、現在の位置が点ｍより距離ｓを越えていることを検知すると加速度を−ｂに変化させ減速し停車する電車をモデル化している。
【数５】
【００４５】
［例３］
別の現実に近い例として、先行研究（Ｒａｊｅｅｖ Ａｌｕｒ， Ｃｏｓｔａｓ Ｃｏｕｒｃｏｕｂｅｔｉｓ， Ｔｈｏｍａｓ Ａ． Ｈｅｎｚｉｎｇｅｒ， aｎｄ Ｐｅｉ−Ｈｓｉｎ Ｈｏ． Ｈｙｂｒｉｄ ａｕｔｏｍａｔａ： Ａｎ ａｌｇｏｒｉｔｈｍｉｃ ａｐｐｒｏａｃｈ ｔｏ ｔｈｅ ｓｐｅｃｉｆｉｃａｔｉｏｎ ａｎｄ ｖｅｒｉｆｉｃａｔｉｏｎ ｏｆ ｈｙｂｒｉｄ ｓｙｓｔｅｍｓ． Ｉｎ Ｈｙｂｒｉｄ Ｓｙｓｔｅｍｓ， ｐａｇｅｓ ２０９-２２９， １９９２．）にて取り上げられている貯水槽モニタのモデルを挙げる。
図２に示すように、この貯水槽１００には給水口１０１と排水口１０２が付いており、給水口１０１のバルブ１０３が開いているときは水位が毎秒１ｃｍで上昇し、バルブ１０３が閉じているときには毎秒２ｃｍで下降する。バルブ１０３の操作はスイッチ１０４で行われており、バルブ１０３の開閉はスイッチ１０４の操作後２秒経ってから起こる。
【００４６】
この貯水槽をモデル化したのが以下のプログラムｃｗａｔｅｒである。変数ｙは水位を、変数ｘはスイッチ操作からの変化時間を、ｓはスイッチの状態(１＝ｏｎ，０＝ｏｆｆ)を、ｖはバルブ１０３の状態（１＝開，０＝閉）を表している。
以下のプログラムにおいて、ｃａｓｅ｛・・・｝は、初めから順番に条件を検査し、条件が成り立った部分のプログラムを実行する構文である。
【数６】
【００４７】
［３．検証装置（プログラム論理を用いた検証アルゴリズム）］
ｗｈｉｌｅｄｔ言語によってコーディングされたハイブリッドシステムのモデルは、プログラミング言語的に記述されているため、形式的検証を行うプログラム検証器４５によって検証が可能である。
【００４８】
図１に示すように、検証装置４は、ｗｈｉｌｅｄｔ言語によってコーディングされたハイブリッドシステムのモデルのコード（プログラム）の入力を受け付ける入力部４１を備えている。入力部４１は、システム１内部の他の機能（例えば、図１の変換器３）から、コードの入力を受け付けても良いし、システム１の外部からコードの入力を受け付けても良い。
【００４９】
モデルのコード等の入力部４１によって受け付けたデータは、記憶部４２によって記憶される。記憶部４２に記憶されたコード等に対して、検証の前処理を行う処理部（セクション化部４３、ループ不変表明計算部４４）が、所定の前処理を行い、その前処理の結果を、再び、記憶部４２に記憶させる。
【００５０】
また、プログラム検証器４５は、記憶部４２に記憶されたコード（必要に応じて前処理の施された後のコード）に対して、形式的検証によって検証を行う。プログラム検証器４５は、検証条件を生成するための検証条件生成器４６と、検証条件として生成された論理式を証明する定理証明器４７と、を有している。
さらに、検証装置４は、定理証明器４７による証明結果（検証結果）を、ハイブリッドシステムの検証結果として出力するための出力部４８を備えている。
【００５１】
検証装置４の入力部４１は、検証対象のプログラムのコード（ハイブリッドシステムの動作をｗｈｉｌｅｄｔ言語でコーディングしたコード）ｃと、当該プログラムの実行前に必ず成り立っているべき条件(事前条件)Ｑと、を入力として受け取る。事前条件Ｑは、ハイブリッドシステムの品質を保証するための品質保証条件となる論理式である。なお、品質保証条件は、プログラムの実行後に必ず成り立っているべき条件（事後条件）など、他の条件であってもよい。
【００５２】
コードｃ中には、ａｓｓｅｒｔ（Ｑ’）（ただし、Ｑ’は、プログラム変数に関する論理式）という文が各所に記述されている。検証装置４の出力部４８は、与えられた事前条件Ｑが成り立つ状態でプログラムがモデル化しているハイブリッドシステムの実行を開始したと考えた場合に、プログラムｃ中のａｓｓｅｒｔ（Ｑ’）で示された論理式が必ず成り立つならば「検証成功」、成り立たない場合があるならば「検証失敗」を、出力する。
【００５３】
検証装置４による検証アルゴリズムにおける具体的な手続きは以下の通りである。
１）プログラムｃ、事前条件Ｑについてセクション化の操作を行う（置換ステップ）。
２）セクション化後のプログラムｃについて、ループ不変表明の計算の操作を行う（付加ステップ）。
３）プログラムｃについて検証条件（論理式）の生成を行う（検証ステップ）。
４）検証条件が成り立つことを、定理証明器を用いて証明する。この証明に定理証明器が成功した場合は検証成功、成功しなかった場合は検証失敗を返す（検証ステップ）。
【００５４】
上記のアルゴリズムで検証を行うと、プログラムが与えられた性質を必ず満たすことが数学的に保証される。これにより、ハイブリッドシステムの品質に数学的な保証を与えることができ、ハイブリッドシステムの品質を大きく向上させることが可能となる。
【００５５】
以下、検証アルゴリズムの動作について説明する。以下では、説明の簡略化のため、例１のプログラム例についてアルゴリズムの動作を説明するが、例２、例３のプログラムについてもこのアルゴリズムが正しく動くことは確認済みである。
【００５６】
［３．１ プログラムｃと事前条件Ｑのセクション化］
前記置換ステップでは、セクション化部（置換処理部）４３が、入力として与えられたプログラムｃと事前条件Ｑについてセクション化という操作を行う。セクション化とは、無限小を示す表現であるｄｔを、実数値を示す表現”１／ｉ”に置換する操作である。実数値を示す表現”１／ｉ”は、数値を示す記号”ｉ”を含んでおり、ｉが示す値（の絶対値）が増加したと考えた場合、その増加につれて、表現”１／ｉ”が示す値が０に収束する値を示す表現となっている。つまり、ｉの絶対値が非常に大きくなれば、１／ｉは０に収束する。ここでは、ｉは、正の整数であるとするが、負の整数であってもよい。また、実数値を示す値は、”１／ｉ”に限らず、例えば、”１／（２×ｉ）”または”１／（３×ｉ）”などであってもよい。セクション化の操作によりｗｈｉｌｅｄｔのプログラムｃと事前条件Ｑとが、(無限小の値を含まない)実数上のプログラムｃｉ・論理式Ｑｉに変換される。セクション化により、無限小値を含むプログラムの検証に無限小値を対象としない既存手法（例えば、以下で述べるループ不変表明の計算等）を適用することが可能となる。
【００５７】
例として、前記プログラム例１について、
【数７】
のもとでの検証例を見る。
【００５８】
この例について、セクション化（置換ステップ）の結果得られるプログラムｃｉと論理式Ｑｉは、次のようになる。
【数８】
【００５９】
［３．２ ループ不変表明の計算］
前記付加ステップでは、ループ不変表明計算部４４が、セクション化して得られたプログラムｃｉについてループ不変表明（ｌｏｏｐ ｉｎｖａｒｉａｎｔ ａｓｓｅｒｔｉｏｎ）を計算し、プログラムｃｉに付加する。
【００６０】
ループ不変表明とは、プログラム中のループが、要求される仕様を満たしているか否かを検証するための論理式である。ループ不変表明は、セクション化されたプログラムｃｉ中のループ文において、ループの入口と出口で必ず成り立っているべき論理式として記述される。ループ不変表明計算部４４は、ループ不変表明を構成する論理式を、自動的に生成して、プログラムｃｉ中に付加する。
ループ不変表明を自動生成するアルゴリズムとしては、例えば、Ｓｒｉｒａｍ Ｓａｎｋａｒａｎａｒａｙａｎａｎ、 Ｈｅｎｎｙ Ｂ． Ｓｉｐｍａ， ａｎｄ Ｚｏｈａｒ Ｍａｎｎａ． Ｎｏｎｌｉｎｅａｒ ｌｏｏｐ ｉｎｖａｒｉａｎｔ ｇｅｎｅｒａｔｉｏｎ ｕｓｉｎｇ ｇｒｏｅｂｎｅｒ ｂａｓｅｓ． Ｉｎ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ３１ｓｔ ＡＣＭ ＳＩＧＰＬＡＮ−ＳＩＧＡＣＴ ｓｙｍｐｏｓｉｕｍ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ｏｆ ｐｒｏｇｒａｍｍｉｎｇ ｌａｎｇｕａｇｅｓ， ＰＯＰＬ ’０４， ｐａｇｅｓ ３１８-３２９， Ｎｅｗ Ｙｏｒｋ， ＮＹ， ＵＳＡ，２００４． ＡＣＭ．に開示されているものを利用することができる。ループ不変表明の計算・付加は、手動で行っても良い。
【００６１】
また、ループ不変表明の計算は、プログラムｃｉに、ｗｈｉｌｅ文などのループ文が含まれている場合には、行う必要があるが、ループ文が含まれていない場合は、行う必要がない。
【００６２】
例として、前節のセクション化されたプログラムｃｉについてはループ不変表明として
【数９】
をとることができる。
【００６３】
すなわち、ループの入口と出口において、必ずｔ＝ｎ／ｉとｘ＝（１＋１／ｉ）ｎが成り立つような０以上のｎが存在する。実際に、ｃｉ中のｗｈｉｌｅ文においては初めてループに入る時にはｘ＝１かつｔ＝０が成り立っているので、ｎとして０を取ればループ不変表明は成り立つ。また、ループの入口でループ不変表明が成り立っているときにループ本体を一回実行すると、ｔの値は１／ｉだけ増加し、ｘの値は、（１＋１／ｉ）倍されるので、上記の論理式のｎをｎ＋１と取り直せば、やはりループの出口でもループ不変表明が成り立っている。
【００６４】
［３．３ 検証条件の生成］
プログラム検証器４５の検証条件生成器４６は、記憶部４２に記憶されたプログラム（セクション化され、ループ不変表明が付加されたプログラム）ｃｉ、及び事前条件（セクション化された事前条件）Ｑｉについて、検証条件の生成という手続きを行う。
【００６５】
検証条件とは、記述した性質が確かに成り立つための十分条件である。すなわち、生成された検証条件とＱｉが成り立つ状況下でｃｉを実行すると必ずＱｉ’が成り立つ。
【００６６】
検証条件生成器４６における検証条件生成アルゴリズムは、プログラム論理と呼ばれる手法に基づいて設計されている。
【００６７】
以下に、プログラム論理に基づく検証条件生成アルゴリズムＶＣを示す。
【数１０】
【００６８】
検証条件生成アルゴリズムＶＣでは、プログラムｃ（セクション化され、ループ不変表明が付加されたプログラム）と、事前条件Ｑを受け取り、検証条件を生成する。
アルゴリズムＶＣは、再帰関数ＶＣ１を用いて定義されている。
ＶＣ１（ｃ，Ｑ）は、プログラムｃの実行後に、Ｑが成り立つために、ｃの実行前に成り立っているべき条件を返す。
例えば、ＶＣ１（ｃ１；ｃ２，Ｑ）の定義は、「ＶＣ１（ｃ２，Ｑ）の結果をＱ’’、ＶＣ１（ｃ１，Ｑ’’）の結果をＱ’としたときに、全体の結果はＱ’である」のように読む。
ＶＣは、「ＶＣ１によって返された条件が、事前条件から帰結される」ことを意味する論理式を検証条件として返す。
なお、検証条件生成アルゴリズムにおいて、Ｑ［ｘ−＞ａ］は、Ｑ中の変数ｘをａで置き換える操作を示す。
【００６９】
プログラム論理に基づく検証条件生成アルゴリズムでは、プログラム全体の検証条件が、その部分プログラムの検証条件の組み合わせで計算されている。これにより、巨大なシステム全体の性質を検証する際に、その構成要素の性質を用いて計算することが容易になる。
【００７０】
例１のプログラムについて検証条件生成アルゴリズムＶＣを適用すると、検証条件として以下の論理式が生成される。
【数１１】
なお、Ｑ’’（ｔ，ｘ，ｉ）は、ループ不変表明計算部４４によって計算されたループ不変表明である。
【００７１】
［３．４ 定理証明器を用いた検証条件の証明］
前述のように生成された検証条件が、「有限個のｉを除いて正しい」ことが示されれば、元のｗｈｉｌｅｄｔのプログラムｃは、与えられた性質を必ず満たす。この検証条件（論理式）の証明のため、本実施形態では、定理証明器（Ｔｈｅｏｒｅｍ Ｐｒｏｖｅｒ）４７を用いる。プログラム検証の分野においては、与えられた論理式が成り立つかどうかを自動的に判定する手法（Ｂｅｈｅａｄｓ Ａｋｂａｒｐｏｕｒ ａｎｄ Ｌ． Ｃ． Ｐａｕｌｓｏｎ． Ｍｅｔｉｔａｒｓｋｉ： Ａｎ ａｕｔｏｍａｔｉｃ ｔｈｅｏｒｅｍ ｐｒｏｖｅｒ ｆｏｒ ｒｅａｌ−ｖａｌｕｅｄ ｓｐｅｃｉａｌ ｆｕｎｃｔｉｏｎｓ． Ｊ． Ａｕｔｏｍａｔｅｄ Ｒｅａｓｏｎｉｎｇ，４４（３）：１７５-２０５， ２０１０．）や、一部人間の支援によって判定する手法（Ｔｈｅ Ｃｏｑ Ｄｅｖｅｌｏｐｍｅｎｔ Ｔｅａｍ． Ｒｅｆｅｒｅｎｃｅ Ｍａｎｕａｌ - Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ．ＩＮＲＩＡ， ２０１０． ｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ／ｒｅｆａｎ／．）が知られており、これらの手法を用いて検証条件が成り立つかどうかを判定する。
【００７２】
生成された検証条件をＱｉとすると、前述の「有限個のｉを除いてＱｉが成り立つ」という条件は、論理式を用いて、
【数１２】
と書ける。
【００７３】
したがって、この論理式を定理証明器で証明することによって、元のプログラム中のａｓｓｅｒｔ（Ｑ）が必ず成り立つことが検証できる。
例１のプログラムについての検証条件を整理すると、
【数１３】
が成り立てば、検証条件が成り立つことが分かる。
したがって、定理証明器４７で証明すべき論理式は、
【数１４】
となる。この論理式が成り立つことは、定理証明器４７を用いて証明することが可能である。
【００７４】
［３．５ セクション化について］
上記のアルゴリズムＶＣに先立ちセクション化という操作を行っている。この操作は無限小値を含むプログラムの検証を、実数のみを扱える定理証明器を用いて行うために必要な操作である。本実施形態では、プログラムｃのセクション化を行ってから以降の手続きを行っているが、プログラムｃのセクション化を行わずにループ不変表明の計算と検証条件の生成を行い、その後、検証条件をセクション化して、定理証明器４７に渡しても良い。
【００７５】
また、無限小値を直接扱うことのできる定理証明器を用いることが可能な場合は、セクション化を行うことなく検証条件の生成と定理証明器での証明を行うことが可能である。
また、セクション化の手法は、プログラム論理を用いない他の検証手法をｗｈｉｌｅｄｔで記述されたプログラムの検証を行う場合にも有効である。
【００７６】
［４．検証例］
［４．１ ｗｈｉｌｅｄｔのプログラムの例Ａ］
ｗｈｉｌｅｄｔによってハイブリッドシステムの動作をコーディングしたモデルのプログラムコードＡを、以下に示す。なお、以下のコードにおいて、「＆＆」は、論理積を示す論理演算子である。
【数１５】
【００７７】
［４．２ セクション化］
例Ａのコードをセクション化したコードＡ１を、以下に示す。セクション化により、例Ａのコードに含まれていたｄｔ（無限小を表す記号）が、”１／ｉ”に変換され、無限小ｄｔを含まない形となっている。したがって、既存のソフトウェア検証手法を適用することが可能となっている。
【数１６】
【００７８】
［４．３ ループ不変表明の付加］
セクション化されたコードＡ１に、ループ不変表明を付加したコードＡ２を、以下に示す。
【数１７】
【００７９】
［４．４ 検証条件］
セクション化され、かつ、ループ不変表面が付加されたコードＡ２に対し、事前条件をｔｒｕｅとして、検証条件生成アルゴリズムＶＣを適用して得られる検証条件を、以下に示す。この検証条件は、定理証明器Ｃｏｑ（ｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ／ｒｅｆａｎ／）で扱えるフォーマットで記述されている。なお、実際に定理証明器で証明すべき論理式は、以下に示す論理式の先頭に、「ｅｘｉｓｔｓ ｎ：ｎａｔ，ｉ＞ｎ −＞」を付加したものになる。
【数１８】
【００８０】
［４．５ セクション化せずにループ不変表明を付加］
例ＡのコードＡを、セクション化せずにループ不変表明を付加したコードＡ３を、以下に示す。
【数１９】
【００８１】
［４．６ セクション化せずに生成された検証条件］
セクション化せずにループ不変表明を付加したコードＡ３に対し、事前条件をｔｒｕｅとして、検証条件生成アルゴリズムＶＣを適用して得られる検証条件を、以下に示す。
無限小を直接扱える定理証明器を用いれば、この検証条件の証明を行うことで、コードＡの安全性を示すことができる。無限小を扱える定理証明器としては、（Ｔａｎｉａ Ｂｅｄｒａｘ−Ｗｅｉｓｓ ａｎｄ Ｒｏｌａｎｄｏ Ｃｈｕａｑｕｉ， ＩＮＦＭＡＬ： Ａｎ Ｉｎｆｉｎｉｔｅｓｉｍａｌ Ａｎａｌｙｓｉｓ Ｉｎｔｅｒａｃｔｉｖｅ Ｔｈｅｏｒｅｍ Ｐｒｏｖｅｒ ａｎｄ Ｐｒｏｂｌｅｍ Ｓｏｌｖｅｒ． Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ＸＩＩ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｆ ｔｈｅ Ｃｈｉｌｅａｎ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ Ｓｏｃｉｅｔｙ， Ｓａｎｔｉａｇｏ， Ｃｈｉｌｅ， Ｏｃｔｏｂｅｒ １９９２．）に記載のものがある。以下の検証条件中のｄｔを”１／ｉ”で置き換えたものは、［４．４ 検証条件］で示した検証条件と一致する。
【数２０】
【００８２】
［５．ｗｈｉｌｅｄｔプログラムへの変換］
図３は、図１に示す変換装置３におけるモデル変換処理を示している。図１に示すように、変換装置３は、生成部３ａと、変換テーブル３ｂと、を備えている。
生成部３ａは、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図（モデル）から、ｗｈｉｌｅｄｔ言語でコーディングされたプログラム（ハイブリッドシステムのモデルのコード）を生成する。
変換テーブル３ｂは、ハイブリッドシステムのブロック線図から、ｗｈｉｌｅｄｔ言語のプログラムコードに生成するために、生成部３ａによって参照される。
【００８３】
変換装置３は、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図のデータの入力を受け付けると（ステップＳ１）、コードの生成を開始する。
【００８４】
図４は、コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図の例を示している。このブロック線図は、時刻１で値が０から１になるステップ信号を生成して出力するブロック５１、入力信号の加減算を行って出力するブロック５２、入力信号を増幅して出力するブロック５３ａ，５３ｂ，５３ｃ、入力信号の積分をして出力するブロック５４ａ，５４ｂ等の各種ブロックを備えている。各ブロックは、結線Ｌ１〜Ｌ７によって適宜接続されている。
【００８５】
コンピュータ支援設計システム２によって生成されたハイブリッドシステムのブロック線図のデータには、ブロック線図中のブロック及び結線を示すデータの他、各ブロックに設定されたパラメータ（例えば、入力信号を増幅して出力するブロック５３ａ，５３ｂ，５３ｃであれば、ゲイン値）を示すデータが含まれている。
【００８６】
変換装置３の生成部３ａは、ブロック線図のデータに基づいて、ブロック線図中の各結線Ｌ１〜Ｌ７に対応する変数ｘｉ，ｘｉ’（ｉは、自然数）を生成する（ステップＳ２）。なお、途中で分岐する結線は、１本の結線であるとみなす。ここでは、各結線に対して、ｘｉ，ｘｉ’という２つの変数を生成する。
また、生成部３ａは、ブロック線図中の各ブロック５１，５２，５３ａ，５３ｂ，５３ｃ，５４ａ，５４ｂのうち、内部状態を持つブロック５４ａ，５４ｂについて、状態変数ｓｉ，ｓｉ’（ｉは、自然数）を生成する（ステップＳ３）。なお、積分ブロック５４ａ，５４ｂの場合、内部状態を示す値は、積分値である。状態変数についても、各ブロックに対してｓｉ，ｓｉ’という２つの変数が生成される。
図５は、図４のブロック線図に対して、変数生成処理（ステップＳ２，Ｓ３）を行って生成された変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’を示している。
【００８７】
さらに、生成部３ａは、時間を表す変数ｔを生成する（ステップＳ４）。
続いて、生成部３ａは、ステップＳ２〜４で生成した各変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’，ｔを初期化するコードｃ０を生成する（ステップＳ５）。以下は、各変数を０で初期化したコードｃ０の例を示している。
【数２１】
【００８８】
なお、ブロックに設定されたパラメータ（ブロック線図のデータ中のパラメータ）として、状態変数の初期値が設定されている場合には、設定された初期値が、生成された変数の初期値となるコードｃ０が生成される。
【００８９】
さらに続けて、生成部３ａは、無限小時間後の各変数ｘｉ，ｘｉ’，ｓｉ，ｓｉ’の値を計算して変数を更新するためのコードｃ１を生成する（ステップＳ６）。コードｃ１は、コードｃ１１と、コードｃ１２とからなる。
【００９０】
コードｃ１１は、各ブロックにおける無限小時間後の出力値として、変数ｘｉに基づいて計算される値を、ｘｉ’に代入するコードである（ここでは、ｘｉのｉと、ｘｉ’のｉとは、一般には異なる値である）。
生成部３ａは、ブロック線図中の各ブロックについて、変換テーブル３ｂを参照することで、コードｃ１１を生成する（ステップＳ６ａ）。なお、変換テーブル３ｂは、変換装置３を構成するコンピュータ又はその他の装置の記憶部に記憶されている。
【００９１】
図６は、ブロック線図において用いられるブロックと、ブロックに対応するｗｈｉｌｅｄｔ言語のコードとの対応を規定した変換テーブルの例を示している。なお、図６では、ブロック線図に用いられるブロックとして、Ｓｉｍｕｌｉｎｋで用いられるブロックの一部を例として挙げた。
図６の変換テーブル３ｂの左側が、Ｓｉｍｕｌｉｎｋにおいて用いられるブロックを示しており、変換テーブル３ｂの右側が、各ブロックに対応するｗｈｉｌｅｄｔ言語のコードを示している。
【００９２】
生成部３ａが、コードｃ１１を生成する際には、変換テーブル３ｂ中のｗｈｉｌｅｄｔ言語のコードにおける変数を示す記号のうち、ｘｉ，ｘｉ’，ｘｊは、変換対象のブロックの入力又は出力に接続された結線に割り当てられた変数名に置換される。また、変換テーブル３ｂ中のｗｈｉｌｅｄｔ言語のコードにおける変数を示す記号のうち、ｓｉ，ｓｉ’は、置換対象のブロックに割り当てられた状態変数名に置換される。
また、変換テーブル３ｂ中のｗｈｉｌｅｄｔ言語のコードにおけるその他の変数を示す記号（ｄｔを除く）は、置換対象のブロックに設定されたパラメータ（ブロック線図のデータ中のパラメータ）が示す値に置換される。
【００９３】
生成部３ａが、図５に示すブロック線図に関して、変換テーブル３ｂを参照することで生成したコードｃ１１を以下に示す。
【数２２】
【００９４】
コードｃ１２は、ｘｉ’，ｓｉ’の値を、ｘｉ，ｓｉに代入するコードである（ここでは、ｘｉのｉと、ｘｉ’のｉとは同じ値であり、ｓｉのｉと、ｓｉ’のｉも同じ値である）。
生成部３ａが、図５に示すブロック線図に関して、ｘｉ’，ｓｉ’の値を、ｘｉ，ｓｉに代入するコードとして生成したコードｃ１２を以下に示す。
【数２３】
【００９５】
さらに、生成部３ａは、無限小を示す記号ｄｔを用いて、時間を示す変数ｔを更新するコード（ｗｈｉｌｅ文）を生成し、先に生成したコードｃ０及びコードｃ１を組み合わせて、図５に示すハイブリッドシステムのブロック線図全体の動作を示すコード［ｃ０； ｗｈｉｌｅ （ｔ＜１／ｄｔ） ｛ｃ１；ｔ：＝ｔ＋ｄｔ｝］を生成する。
【００９６】
生成されたコードは、［ｃ０； ｗｈｉｌｅ （ｔ＜１／ｄｔ） ｛ｃ１；ｔ：＝ｔ＋ｄｔ｝］は、コンピュータの記憶部に記憶されて、検証装置４による検証に用いても良いし、表示装置などに出力されてもよい。
【００９７】
なお、変換装置３は、上述の変換処理とは逆の変換を行うことで、ブロック線図によって記述可能なハイブリッドシステムの動作を示すｗｈｉｌｅｄｔ言語のコードを、ブロック線図に変換することもできる。
【００９８】
なお、本実施形態では、ｗｈｉｌｅｄｔ言語のコードを、変換装置によって自動的に作成したが、人手でコーディングを行っても良い。
さらに、本実施形態では、ハイブリッドシステムの開発者として、ソフトウェア技術者を活用することが可能である。
すなわち、ハイブリッドシステムの開発現場では、制御理論に由来する開発手法が主に採用されているため、通常のソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが困難であった。しかし、本実施形態では、ハイブリッドシステムのモデルを、プログラミング言語によってコーディングできるため、プログラミング言語に慣れているソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが可能である。
【００９９】
［６．付記］
なお、上記において開示した事項は、例示であって、本発明を限定するものではなく、様々な変形が可能である。
【符号の説明】
【０１００】
１ システム
２ コンピュータ支援設計システム
３ 変換装置
３ａ 生成部
３ｂ 変換テーブル
４ 検証装置
４１ 入力部
４２ 記憶部
４３ セクション化部（置換処理部）
４４ ループ不変表明計算部
４５ プログラム検証器
４６ 検証条件生成器
４７ 定理証明器
４８ 出力部
【特許請求の範囲】
【請求項１】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされている
ハイブリッドシステムの検証方法。
【請求項２】
前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項１記載のハイブリッドシステムの検証方法。
【請求項３】
前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証する
請求項１又は２記載のハイブリッドシステムの検証方法。
【請求項４】
前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明する
請求項２記載のハイブリッドシステムの検証方法。
【請求項５】
前記数値を表す前記記号は、正の整数を示す記号である
請求項３又は４記載のハイブリッドシステムの検証方法。
【請求項６】
前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含む
請求項１〜５のいずれか１項に記載のハイブリッドシステムの検証方法。
【請求項７】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備えているハイブリッドシステムの検証装置。
【請求項８】
前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項７記載のハイブリッドシステムの検証装置。
【請求項９】
前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証する
請求項７又は８記載のハイブリッドシステムの検証装置。
【請求項１０】
前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明する
請求項８記載のハイブリッドシステムの検証装置。
【請求項１１】
前記数値を表す前記記号は、正の整数を示す記号である
請求項９又は１０記載のハイブリッドシステムの検証装置。
【請求項１２】
前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備える
請求項７〜１１のいずれか１項に記載のハイブリッドシステムの検証装置。
【請求項１３】
コンピュータを、請求項７〜１２のいずれか１項に記載の検証装置として機能させるためのコンピュータプログラム。
【請求項１４】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法。
【請求項１５】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置あって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置。
【請求項１６】
コンピュータを、請求項１５記載のモデル変換装置として機能させるためのコンピュータプログラム。
【請求項１】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされている
ハイブリッドシステムの検証方法。
【請求項２】
前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項１記載のハイブリッドシステムの検証方法。
【請求項３】
前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証する
請求項１又は２記載のハイブリッドシステムの検証方法。
【請求項４】
前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明する
請求項２記載のハイブリッドシステムの検証方法。
【請求項５】
前記数値を表す前記記号は、正の整数を示す記号である
請求項３又は４記載のハイブリッドシステムの検証方法。
【請求項６】
前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含む
請求項１〜５のいずれか１項に記載のハイブリッドシステムの検証方法。
【請求項７】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備えているハイブリッドシステムの検証装置。
【請求項８】
前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項７記載のハイブリッドシステムの検証装置。
【請求項９】
前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証する
請求項７又は８記載のハイブリッドシステムの検証装置。
【請求項１０】
前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて０に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明する
請求項８記載のハイブリッドシステムの検証装置。
【請求項１１】
前記数値を表す前記記号は、正の整数を示す記号である
請求項９又は１０記載のハイブリッドシステムの検証装置。
【請求項１２】
前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備える
請求項７〜１１のいずれか１項に記載のハイブリッドシステムの検証装置。
【請求項１３】
コンピュータを、請求項７〜１２のいずれか１項に記載の検証装置として機能させるためのコンピュータプログラム。
【請求項１４】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法。
【請求項１５】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置あって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置。
【請求項１６】
コンピュータを、請求項１５記載のモデル変換装置として機能させるためのコンピュータプログラム。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図２】
【図３】
【図４】
【図５】
【図６】
【公開番号】特開２０１３−３８９７（Ｐ２０１３−３８９７Ａ）
【公開日】平成２５年１月７日（２０１３．１．７）
【国際特許分類】
【出願番号】特願２０１１−１３５２０１（Ｐ２０１１−１３５２０１）
【出願日】平成２３年６月１７日（２０１１．６．１７）
【出願人】（５０４１３２２７２）国立大学法人京都大学 (1,269)
【Ｆターム（参考）】
【公開日】平成２５年１月７日（２０１３．１．７）
【国際特許分類】
【出願日】平成２３年６月１７日（２０１１．６．１７）
【出願人】（５０４１３２２７２）国立大学法人京都大学 (1,269)
【Ｆターム（参考）】
[ Back to top ]