"連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、を含み、前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされているハイブリッドシステムの検証方法。前記プログラム検証器は、定理証明器を含み、前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する請求項1記載のハイブリッドシステムの検証方法。前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証する請求項1又は2記載のハイブリッドシステムの検証方法。前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明する請求項2記載のハイブリッドシステムの検証方法。前記数値を表す前記記号は、正の整数を示す記号である請求項3又は4記載のハイブリッドシステムの検証方法。前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含む請求項1~5のいずれか1項に記載のハイブリッドシステムの検証方法。連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、を備えているハイブリッドシステムの検証装置。前記プログラム検証器は、定理証明器を含み、前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する請求項7記載のハイブリッドシステムの検証装置。前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証する請求項7又は8記載のハイブリッドシステムの検証装置。前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明する請求項8記載のハイブリッドシステムの検証装置。前記数値を表す前記記号は、正の整数を示す記号である請求項9又は10記載のハイブリッドシステムの検証装置。前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備える請求項7~11のいずれか1項に記載のハイブリッドシステムの検証装置。コンピュータを、請求項7~12のいずれか1項に記載の検証装置として機能させるためのコンピュータプログラム。連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成されるハイブリッドシステムのモデル変換方法。連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置あって、前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成するハイブリッドシステムのモデル変換装置。コンピュータを、請求項15記載のモデル変換装置として機能させるためのコンピュータプログラム。ここで、ハイブリッドシステムが意図した通りに動作することを検証することは非常に重要な問題である。一般に、システムが意図した通りに振る舞うことを検証するために、シミュレーションによるテストがよく用いられる。これは、様々な入力をシステムに繰り返し与え、その動作が意図した通りであることを確認することで、システムの品質を担保しようとする手法である。例えば、Simulinkを用いてハイブリッドシステムの開発を行う場合には、Simulink上で図式によって表現されたハイブリッドシステムに対して、いろいろな信号を入力として与えて、そのハイブリッドシステムの振る舞いをSimulink上で確認することで、ハイブリッドシステムの品質をチェックすることができる。しかしながら、シミュレーションによるテストに基づく品質チェックのみでは、全ての入力を網羅することが不可能である。したがって、シミュレーションの際に用いなかった入力に対しての品質の担保が全く無い。そこで、本発明は、ハイブリッドシステムの検証のための新たな技術的手段を提供することを目的とする。1本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、を含み、前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、前記モデルは、前記ハイブリッドシステムにおける前記連続値の変化が、前記無限小を用いてコーディングされているハイブリッドシステムの検証方法である。2前記プログラム検証器は、定理証明器を含み、前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。3前記検証ステップに先立って、前記モデルのコードにおける無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証するのが好ましい。4前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換ステップを更に含み、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。5前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。6前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含むのが好ましい。7他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、を備えているハイブリッドシステムの検証装置である。8前記プログラム検証器は、定理証明器を含み、前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証するのが好ましい。9前記記憶部に記憶されている前記モデルのコードにおける無限小を示す表現を、実数値を示す表現形式に置換する置換処理部を更に備え、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証するのが好ましい。10前記検証条件を示す論理式における無限小を示す表現を、実数値を示す表現に置換する置換処理部を更に備え、前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明するのが好ましい。11前記数値を表す前記記号は、正の整数を示す記号であるのが好ましい。12前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備えるのが好ましい。13他の観点からみた本発明は、コンピュータを、前記7~12のいずれか1項に記載の検証装置として機能させるためのコンピュータプログラムである。14他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成ステップを含み、前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードが生成されるハイブリッドシステムのモデル変換方法である。15他の観点からみた本発明は、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置であって、前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、前記プログラミング言語は、無限小を記述可能なプログラミング言語であり、前記生成部は、前記ハイブリッドシステムにおける前記連続値の変化を、前記無限小を用いてコーディングしたコードを生成するハイブリッドシステムのモデル変換装置である。16他の観点からみた本発明は、コンピュータを、前記15のモデル変換装置として機能させるためのコンピュータプログラムである。以下、本発明の好ましい実施形態について添付図面を参照しながら説明する。[1.ハイブリッドシステムの設計支援及び検証のためのシステム]図1は、ハイブリッドシステムの設計支援及び検証のためのシステム1を示している。このシステム1は、ハイブリッドシステムの作成を行うことができるコンピュータ支援設計システム2と、コンピュータ支援設計システム2で作成したハイブリッドシステムを、ハイブリッドシステムをモデル化したプログラムに変換する変換器と、プログラミング言語によってコーディングされたハイブリッドシステムを検証する検証装置4と、を備えている。なお、システム1の各機能は、コンピュータの記憶装置にインストールされたコンピュータプログラムが、コンピュータに実行されることによって発揮される。そのコンピュータプログラムは、記録媒体に記録して、譲渡販売することができる。本実施形態では、ハイブリッドシステムを検証するために、コンピュータ支援設計システム2で作成したハイブリッドシステムに対して、様々な入力を与えてシミュレーションを行うのではなく、プログラムに対する形式的検証を用いて検証を行う。ここで、プログラムソフトウェアの開発においては、形式的検証形式的手法によるプログラム検証による検証が用いられつつある。形式的検証とは、数理科学的に正しさが証明されたアルゴリズム例えば、定理証明器で、プログラムを解析し、プログラムにバグが無いことを保証する手法である。なお、形式的検証については、例えば、林晋、プログラム検証論、共立出版、1994に開示されている。形式的検証では、様々な入力を与えてテストすることなく、すべての入力について網羅的にテストを行ったのと同じ結果が得られる。様々な入力を与えてテストすることで検証を行う方法では、システムをモジュール化した場合に、モジュール毎の品質保証ができたとしても、モジュールを組み合わせたシステム全体の品質保証が困難である。しかし、形式的検証には、モジュール毎の品質保証によって、モジュールを組み合わせたシステム全体の品質保証が可能な技術が多く存在するので、モジュール性を確保することが容易である。このように、形式的検証は、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易である。このように優れた特性を持つ形式的検証の手法を、ハイブリッドシステムの検証に利用するという点が、本発明者らの着想の第一点である。そして、本発明者らの着想の第二点は、プログラミング言語を、ハイブリッドシステムの動作の記述に用いることである。プログラミング言語は、元来、コンピュータによって実行されるプログラムコードを記述するためのものであり、ハイブリッドシステムの動作を記述するものではない。従来のプログラミング言語であっても、ハイブリッドシステムの動作のうち、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値の変化は、当然に、記述できる。しかし、ハイブリッドシステムの動作には、ソフトウェアによって制御されるがソフトウェアの動作そのものではない連続値速度や温度のような物理量の変化も含まれる。従来、ソフトウェアの動作ではない連続値の変化そのものは、プログラミング言語による記述の対象になっていない。これに対して、本実施形態のシステム1では、ハイブリッドシステムの記述のために拡張されたプログラミング言語が用いられる。その拡張されたプログラミング言語モデリング言語によって、連続値の変化を含むハイブリッドシステムの動作が、モデリングされる。そして、拡張されたプログラミング言語を用いてモデリングされたハイブリッドシステムを、プログラム検証技術である形式的検証の手法によって検証する。これにより、ハイブリッドシステムを、プログラムの検証と同様の手法で検証でき、様々な入力を与えてテストする必要がなく、モジュール性の確保が容易となる。[2.ハイブリッドシステムのモデリング言語]本実施形態では、手続き型プログラミング言語のエッセンスであるwhile言語GlynnWinskel.FormalSemanticsofProgrammingLanguages.TheMITPress,February1993.を、無限小の値を表すdtという記号で拡張した言語であるwhiledtを用いる。無限小の値を言語に加えることにより、連続量を扱うシステムを、手続き型プログラミング言語で記述することができる。つまり、プログラミング言語は、元来、ソフトウェアの動作に関わる離散値を記述できるものであるから、無限小の導入によって連続値が記述可能となれば、連続値と離散値とが相互に影響を及ぼしあって変化するハイブリッドシステムの動作が記述可能となる。なお、無限小を導入したプログラミング言語whiledt言語は、コンピュータによる実行を前提としたものではなく、ハイブリッドシステムの動作を記述するための言語である。したがって、無限小を導入したプログラミング言語は、ハイブリッドシステムのモデリング言語ということができる。[2.1モデリング言語whiledtの仕様]以下に、本実施形態で用いられるwhiledt言語の定義の例を示す。whiledt言語の定義は、BNF記法で記述されており、例えば、a::=x|r|dt|a1aopa2は、aは、x,r,dtもしくはa1aopa2のいずれかであるという意味である。aは、算術式で、変数、実数定数、無限小を表す記号dtか、算術演算aopのいずれかである。bは、真偽値を表す式で、真を表す値、偽を表す値、ブール演算and演算、or演算またはnot演算または算術式間の関係式a1<a2等のいずれかである。cはコマンドプログラムで実行される文であり、それぞれの意味は以下の通りである。skip:なにも実行せずに終了する。x:=a:算術式aを評価し、その評価結果を変数xに代入する。c1;c2:コマンドc1を実行し、その後コマンドc2を実行する。ifbthenc1elsec2:式bを評価し、その結果が真ならばc1を実行し、偽ならばc2を実行する。whileQbdocdone:式bが真である間、cを繰り返し実行する。上記のように、whiledt言語の定義では、算術式aの定義に、無限小を示す記号dtが導入されている。無限小を示す記号dtに関する定義の部分を除くと、whiledt言語の定義は、一般的な手続き型プログラミング言語に準拠したものとなっている。つまり、whiledt言語は、手続き型プログラミング言語を、無限小が記述できるように拡張した言語、ということができる。なお、whiledt言語の定義は、上記のものに限られず、さらに拡張されていてもよい。本実施形態では、算術演算aopに累乗を含めるなど、上記定義をさらに拡張したものを用いる。[2.2whiledt言語によるプログラム例モデル例][例1]初めに非常にシンプルなwhiledtのプログラム例を示す。このプログラムは微分方程式に従ったxの時間発展を時刻5まで計算する。whileコマンドの各ループにおいて、xの値は微分方程式で指定された現時刻でのxの微小変化量だけ変化する。プログラム中のassertx≧2aは、この時点においてx≧2aが成り立たなければならないということを表しており、この条件が必ず成り立つことを、後述のプログラム論理を用いて検証する。[例2]他の一例として先行研究AndrePlatzer.Differentialdynamiclogicforhybridsystems.J.Autom.Reasoning,412143189,2008.にて取り上げられているヨーロッパ鉄道制御システムETCSのモデルを挙げる。Caccelは定数加速度aで時刻εまで加速する電車をモデル化している。ここで変数vは電車の速度、変数zは電車の位置を表現している。whileループで時刻tを無限小量ずつ変化させ、コマンドCdrive内ではv:=va×dtで速度vを、加速度aに応じて変化させ、z:zv×dtで電車の位置zを現在の速度vに応じて変化させている。また、以下のプログラムcchkAndBrakeは、電車の位置を時間間隔εでモニタリングし、現在の位置が点mより距離sを越えていることを検知すると加速度を-bに変化させ減速し停車する電車をモデル化している。[例3]別の現実に近い例として、先行研究RajeevAlur,CostasCourcoubetis,ThomasA.Henzinger,andPei-HsinHo.Hybridautomata:Analgorithmicapproachtothespecificationandverificationofhybridsystems.InHybridSystems,pages209229,1992.にて取り上げられている貯水槽モニタのモデルを挙げる。図2に示すように、この貯水槽100には給水口101と排水口102が付いており、給水口101のバルブ103が開いているときは水位が毎秒1cmで上昇し、バルブ103が閉じているときには毎秒2cmで下降する。バルブ103の操作はスイッチ104で行われており、バルブ103の開閉はスイッチ104の操作後2秒経ってから起こる。この貯水槽をモデル化したのが以下のプログラムcwaterである。変数yは水位を、変数xはスイッチ操作からの変化時間を、sはスイッチの状態を、vはバルブ103の状態1=開,0=閉を表している。以下のプログラムにおいて、case{}は、初めから順番に条件を検査し、条件が成り立った部分のプログラムを実行する構文である。[3.検証装置プログラム論理を用いた検証アルゴリズム]whiledt言語によってコーディングされたハイブリッドシステムのモデルは、プログラミング言語的に記述されているため、形式的検証を行うプログラム検証器45によって検証が可能である。図1に示すように、検証装置4は、whiledt言語によってコーディングされたハイブリッドシステムのモデルのコードプログラムの入力を受け付ける入力部41を備えている。入力部41は、システム1内部の他の機能例えば、図1の変換器3から、コードの入力を受け付けても良いし、システム1の外部からコードの入力を受け付けても良い。モデルのコード等の入力部41によって受け付けたデータは、記憶部42によって記憶される。記憶部42に記憶されたコード等に対して、検証の前処理を行う処理部セクション化部43、ループ不変表明計算部44が、所定の前処理を行い、その前処理の結果を、再び、記憶部42に記憶させる。また、プログラム検証器45は、記憶部42に記憶されたコード必要に応じて前処理の施された後のコードに対して、形式的検証によって検証を行う。プログラム検証器45は、検証条件を生成するための検証条件生成器46と、検証条件として生成された論理式を証明する定理証明器47と、を有している。さらに、検証装置4は、定理証明器47による証明結果検証結果を、ハイブリッドシステムの検証結果として出力するための出力部48を備えている。検証装置4の入力部41は、検証対象のプログラムのコードハイブリッドシステムの動作をwhiledt言語でコーディングしたコードcと、当該プログラムの実行前に必ず成り立っているべき条件Qと、を入力として受け取る。事前条件Qは、ハイブリッドシステムの品質を保証するための品質保証条件となる論理式である。なお、品質保証条件は、プログラムの実行後に必ず成り立っているべき条件事後条件など、他の条件であってもよい。コードc中には、assertQ’ただし、Q’は、プログラム変数に関する論理式という文が各所に記述されている。検証装置4の出力部48は、与えられた事前条件Qが成り立つ状態でプログラムがモデル化しているハイブリッドシステムの実行を開始したと考えた場合に、プログラムc中のassertQ’で示された論理式が必ず成り立つならば検証成功、成り立たない場合があるならば検証失敗を、出力する。検証装置4による検証アルゴリズムにおける具体的な手続きは以下の通りである。1プログラムc、事前条件Qについてセクション化の操作を行う置換ステップ。2セクション化後のプログラムcについて、ループ不変表明の計算の操作を行う付加ステップ。3プログラムcについて検証条件論理式の生成を行う検証ステップ。4検証条件が成り立つことを、定理証明器を用いて証明する。この証明に定理証明器が成功した場合は検証成功、成功しなかった場合は検証失敗を返す検証ステップ。上記のアルゴリズムで検証を行うと、プログラムが与えられた性質を必ず満たすことが数学的に保証される。これにより、ハイブリッドシステムの品質に数学的な保証を与えることができ、ハイブリッドシステムの品質を大きく向上させることが可能となる。以下、検証アルゴリズムの動作について説明する。以下では、説明の簡略化のため、例1のプログラム例についてアルゴリズムの動作を説明するが、例2、例3のプログラムについてもこのアルゴリズムが正しく動くことは確認済みである。[3.1プログラムcと事前条件Qのセクション化]前記置換ステップでは、セクション化部置換処理部43が、入力として与えられたプログラムcと事前条件Qについてセクション化という操作を行う。セクション化とは、無限小を示す表現であるdtを、実数値を示す表現1/iに置換する操作である。実数値を示す表現1/iは、数値を示す記号iを含んでおり、iが示す値の絶対値が増加したと考えた場合、その増加につれて、表現1/iが示す値が0に収束する値を示す表現となっている。つまり、iの絶対値が非常に大きくなれば、1/iは0に収束する。ここでは、iは、正の整数であるとするが、負の整数であってもよい。また、実数値を示す値は、1/iに限らず、例えば、1/2×iまたは1/3×iなどであってもよい。セクション化の操作によりwhiledtのプログラムcと事前条件Qとが、実数上のプログラムci論理式Qiに変換される。セクション化により、無限小値を含むプログラムの検証に無限小値を対象としない既存手法例えば、以下で述べるループ不変表明の計算等を適用することが可能となる。例として、前記プログラム例1について、のもとでの検証例を見る。この例について、セクション化置換ステップの結果得られるプログラムciと論理式Qiは、次のようになる。[3.2ループ不変表明の計算]前記付加ステップでは、ループ不変表明計算部44が、セクション化して得られたプログラムciについてループ不変表明loopinvariantassertionを計算し、プログラムciに付加する。ループ不変表明とは、プログラム中のループが、要求される仕様を満たしているか否かを検証するための論理式である。ループ不変表明は、セクション化されたプログラムci中のループ文において、ループの入口と出口で必ず成り立っているべき論理式として記述される。ループ不変表明計算部44は、ループ不変表明を構成する論理式を、自動的に生成して、プログラムci中に付加する。ループ不変表明を自動生成するアルゴリズムとしては、例えば、SriramSankaranarayanan、HennyB.Sipma,andZoharManna.Nonlinearloopinvariantgenerationusinggroebnerbases.InProceedingsofthe31stACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages,POPL’04,pages318329,NewYork,NY,USA,2004.ACM.に開示されているものを利用することができる。ループ不変表明の計算付加は、手動で行っても良い。また、ループ不変表明の計算は、プログラムciに、while文などのループ文が含まれている場合には、行う必要があるが、ループ文が含まれていない場合は、行う必要がない。例として、前節のセクション化されたプログラムciについてはループ不変表明としてをとることができる。すなわち、ループの入口と出口において、必ずt=n/iとx=11/inが成り立つような0以上のnが存在する。実際に、ci中のwhile文においては初めてループに入る時にはx=1かつt=0が成り立っているので、nとして0を取ればループ不変表明は成り立つ。また、ループの入口でループ不変表明が成り立っているときにループ本体を一回実行すると、tの値は1/iだけ増加し、xの値は、11/i倍されるので、上記の論理式のnをn1と取り直せば、やはりループの出口でもループ不変表明が成り立っている。[3.3検証条件の生成]プログラム検証器45の検証条件生成器46は、記憶部42に記憶されたプログラムセクション化され、ループ不変表明が付加されたプログラムci、及び事前条件セクション化された事前条件Qiについて、検証条件の生成という手続きを行う。検証条件とは、記述した性質が確かに成り立つための十分条件である。すなわち、生成された検証条件とQiが成り立つ状況下でciを実行すると必ずQi’が成り立つ。検証条件生成器46における検証条件生成アルゴリズムは、プログラム論理と呼ばれる手法に基づいて設計されている。以下に、プログラム論理に基づく検証条件生成アルゴリズムVCを示す。検証条件生成アルゴリズムVCでは、プログラムcセクション化され、ループ不変表明が付加されたプログラムと、事前条件Qを受け取り、検証条件を生成する。アルゴリズムVCは、再帰関数VC1を用いて定義されている。VC1c,Qは、プログラムcの実行後に、Qが成り立つために、cの実行前に成り立っているべき条件を返す。例えば、VC1c1;c2,Qの定義は、VC1c2,Qの結果をQ’’、VC1c1,Q’’の結果をQ’としたときに、全体の結果はQ’であるのように読む。VCは、VC1によって返された条件が、事前条件から帰結されることを意味する論理式を検証条件として返す。なお、検証条件生成アルゴリズムにおいて、Q[x->a]は、Q中の変数xをaで置き換える操作を示す。プログラム論理に基づく検証条件生成アルゴリズムでは、プログラム全体の検証条件が、その部分プログラムの検証条件の組み合わせで計算されている。これにより、巨大なシステム全体の性質を検証する際に、その構成要素の性質を用いて計算することが容易になる。例1のプログラムについて検証条件生成アルゴリズムVCを適用すると、検証条件として以下の論理式が生成される。なお、Q’’t,x,iは、ループ不変表明計算部44によって計算されたループ不変表明である。[3.4定理証明器を用いた検証条件の証明]前述のように生成された検証条件が、有限個のiを除いて正しいことが示されれば、元のwhiledtのプログラムcは、与えられた性質を必ず満たす。この検証条件論理式の証明のため、本実施形態では、定理証明器TheoremProver47を用いる。プログラム検証の分野においては、与えられた論理式が成り立つかどうかを自動的に判定する手法BeheadsAkbarpourandL.C.Paulson.Metitarski:Anautomatictheoremproverforreal-valuedspecialfunctions.J.AutomatedReasoning,443:175205,2010.や、一部人間の支援によって判定する手法TheCoqDevelopmentTeam.ReferenceManualTheCoqProofAssistant.INRIA,2010.http://coq.inria.fr/refan/.が知られており、これらの手法を用いて検証条件が成り立つかどうかを判定する。生成された検証条件をQiとすると、前述の有限個のiを除いてQiが成り立つという条件は、論理式を用いて、と書ける。したがって、この論理式を定理証明器で証明することによって、元のプログラム中のassertQが必ず成り立つことが検証できる。例1のプログラムについての検証条件を整理すると、が成り立てば、検証条件が成り立つことが分かる。したがって、定理証明器47で証明すべき論理式は、となる。この論理式が成り立つことは、定理証明器47を用いて証明することが可能である。[3.5セクション化について]上記のアルゴリズムVCに先立ちセクション化という操作を行っている。この操作は無限小値を含むプログラムの検証を、実数のみを扱える定理証明器を用いて行うために必要な操作である。本実施形態では、プログラムcのセクション化を行ってから以降の手続きを行っているが、プログラムcのセクション化を行わずにループ不変表明の計算と検証条件の生成を行い、その後、検証条件をセクション化して、定理証明器47に渡しても良い。また、無限小値を直接扱うことのできる定理証明器を用いることが可能な場合は、セクション化を行うことなく検証条件の生成と定理証明器での証明を行うことが可能である。また、セクション化の手法は、プログラム論理を用いない他の検証手法をwhiledtで記述されたプログラムの検証を行う場合にも有効である。[4.検証例][4.1whiledtのプログラムの例A]whiledtによってハイブリッドシステムの動作をコーディングしたモデルのプログラムコードAを、以下に示す。なお、以下のコードにおいて、は、論理積を示す論理演算子である。[4.2セクション化]例Aのコードをセクション化したコードA1を、以下に示す。セクション化により、例Aのコードに含まれていたdt無限小を表す記号が、1/iに変換され、無限小dtを含まない形となっている。したがって、既存のソフトウェア検証手法を適用することが可能となっている。[4.3ループ不変表明の付加]セクション化されたコードA1に、ループ不変表明を付加したコードA2を、以下に示す。[4.4検証条件]セクション化され、かつ、ループ不変表面が付加されたコードA2に対し、事前条件をtrueとして、検証条件生成アルゴリズムVCを適用して得られる検証条件を、以下に示す。この検証条件は、定理証明器Coqhttp://coq.inria.fr/refan/で扱えるフォーマットで記述されている。なお、実際に定理証明器で証明すべき論理式は、以下に示す論理式の先頭に、existsn:nat,i>n->を付加したものになる。[4.5セクション化せずにループ不変表明を付加]例AのコードAを、セクション化せずにループ不変表明を付加したコードA3を、以下に示す。[4.6セクション化せずに生成された検証条件]セクション化せずにループ不変表明を付加したコードA3に対し、事前条件をtrueとして、検証条件生成アルゴリズムVCを適用して得られる検証条件を、以下に示す。無限小を直接扱える定理証明器を用いれば、この検証条件の証明を行うことで、コードAの安全性を示すことができる。無限小を扱える定理証明器としては、TaniaBedrax-WeissandRolandoChuaqui,INFMAL:AnInfinitesimalAnalysisInteractiveTheoremProverandProblemSolver.ProceedingsoftheXIIInternationalConferenceoftheChileanComputerScienceSociety,Santiago,Chile,October1992.に記載のものがある。以下の検証条件中のdtを1/iで置き換えたものは、[4.4検証条件]で示した検証条件と一致する。[5.whiledtプログラムへの変換]図3は、図1に示す変換装置3におけるモデル変換処理を示している。図1に示すように、変換装置3は、生成部3aと、変換テーブル3bと、を備えている。生成部3aは、コンピュータ支援設計システム2によって生成されたハイブリッドシステムのブロック線図モデルから、whiledt言語でコーディングされたプログラムハイブリッドシステムのモデルのコードを生成する。変換テーブル3bは、ハイブリッドシステムのブロック線図から、whiledt言語のプログラムコードに生成するために、生成部3aによって参照される。変換装置3は、コンピュータ支援設計システム2によって生成されたハイブリッドシステムのブロック線図のデータの入力を受け付けるとステップS1、コードの生成を開始する。図4は、コンピュータ支援設計システム2によって生成されたハイブリッドシステムのブロック線図の例を示している。このブロック線図は、時刻1で値が0から1になるステップ信号を生成して出力するブロック51、入力信号の加減算を行って出力するブロック52、入力信号を増幅して出力するブロック53a,53b,53c、入力信号の積分をして出力するブロック54a,54b等の各種ブロックを備えている。各ブロックは、結線L1~L7によって適宜接続されている。コンピュータ支援設計システム2によって生成されたハイブリッドシステムのブロック線図のデータには、ブロック線図中のブロック及び結線を示すデータの他、各ブロックに設定されたパラメータ例えば、入力信号を増幅して出力するブロック53a,53b,53cであれば、ゲイン値を示すデータが含まれている。変換装置3の生成部3aは、ブロック線図のデータに基づいて、ブロック線図中の各結線L1~L7に対応する変数xi,xi’iは、自然数を生成するステップS2。なお、途中で分岐する結線は、1本の結線であるとみなす。ここでは、各結線に対して、xi,xi’という2つの変数を生成する。また、生成部3aは、ブロック線図中の各ブロック51,52,53a,53b,53c,54a,54bのうち、内部状態を持つブロック54a,54bについて、状態変数si,si’iは、自然数を生成するステップS3。なお、積分ブロック54a,54bの場合、内部状態を示す値は、積分値である。状態変数についても、各ブロックに対してsi,si’という2つの変数が生成される。図5は、図4のブロック線図に対して、変数生成処理ステップS2,S3を行って生成された変数xi,xi’,si,si’を示している。さらに、生成部3aは、時間を表す変数tを生成するステップS4。続いて、生成部3aは、ステップS2~4で生成した各変数xi,xi’,si,si’,tを初期化するコードc0を生成するステップS5。以下は、各変数を0で初期化したコードc0の例を示している。なお、ブロックに設定されたパラメータブロック線図のデータ中のパラメータとして、状態変数の初期値が設定されている場合には、設定された初期値が、生成された変数の初期値となるコードc0が生成される。さらに続けて、生成部3aは、無限小時間後の各変数xi,xi’,si,si’の値を計算して変数を更新するためのコードc1を生成するステップS6。コードc1は、コードc11と、コードc12とからなる。コードc11は、各ブロックにおける無限小時間後の出力値として、変数xiに基づいて計算される値を、xi’に代入するコードであるここでは、xiのiと、xi’のiとは、一般には異なる値である。生成部3aは、ブロック線図中の各ブロックについて、変換テーブル3bを参照することで、コードc11を生成するステップS6a。なお、変換テーブル3bは、変換装置3を構成するコンピュータ又はその他の装置の記憶部に記憶されている。図6は、ブロック線図において用いられるブロックと、ブロックに対応するwhiledt言語のコードとの対応を規定した変換テーブルの例を示している。なお、図6では、ブロック線図に用いられるブロックとして、Simulinkで用いられるブロックの一部を例として挙げた。図6の変換テーブル3bの左側が、Simulinkにおいて用いられるブロックを示しており、変換テーブル3bの右側が、各ブロックに対応するwhiledt言語のコードを示している。生成部3aが、コードc11を生成する際には、変換テーブル3b中のwhiledt言語のコードにおける変数を示す記号のうち、xi,xi’,xjは、変換対象のブロックの入力又は出力に接続された結線に割り当てられた変数名に置換される。また、変換テーブル3b中のwhiledt言語のコードにおける変数を示す記号のうち、si,si’は、置換対象のブロックに割り当てられた状態変数名に置換される。また、変換テーブル3b中のwhiledt言語のコードにおけるその他の変数を示す記号dtを除くは、置換対象のブロックに設定されたパラメータブロック線図のデータ中のパラメータが示す値に置換される。生成部3aが、図5に示すブロック線図に関して、変換テーブル3bを参照することで生成したコードc11を以下に示す。コードc12は、xi’,si’の値を、xi,siに代入するコードであるここでは、xiのiと、xi’のiとは同じ値であり、siのiと、si’のiも同じ値である。生成部3aが、図5に示すブロック線図に関して、xi’,si’の値を、xi,siに代入するコードとして生成したコードc12を以下に示す。さらに、生成部3aは、無限小を示す記号dtを用いて、時間を示す変数tを更新するコードwhile文を生成し、先に生成したコードc0及びコードc1を組み合わせて、図5に示すハイブリッドシステムのブロック線図全体の動作を示すコード[c0;whilet<1/dt{c1;t:=tdt}]を生成する。生成されたコードは、[c0;whilet<1/dt{c1;t:=tdt}]は、コンピュータの記憶部に記憶されて、検証装置4による検証に用いても良いし、表示装置などに出力されてもよい。なお、変換装置3は、上述の変換処理とは逆の変換を行うことで、ブロック線図によって記述可能なハイブリッドシステムの動作を示すwhiledt言語のコードを、ブロック線図に変換することもできる。なお、本実施形態では、whiledt言語のコードを、変換装置によって自動的に作成したが、人手でコーディングを行っても良い。さらに、本実施形態では、ハイブリッドシステムの開発者として、ソフトウェア技術者を活用することが可能である。すなわち、ハイブリッドシステムの開発現場では、制御理論に由来する開発手法が主に採用されているため、通常のソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが困難であった。しかし、本実施形態では、ハイブリッドシステムのモデルを、プログラミング言語によってコーディングできるため、プログラミング言語に慣れているソフトウェア技術者を、ハイブリッドシステムの開発者として活用することが可能である。[6.付記]なお、上記において開示した事項は、例示であって、本発明を限定するものではなく、様々な変形が可能である。"