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)
FI G06F 17/50 612L
G06F 17/50 664Z
G06F 9/06 620R
請求項の数または発明の数 17
全頁数 26
出願番号 特願2011-135201 (P2011-135201)
出願日 平成23年6月17日(2011.6.17)
審査請求日 平成26年5月30日(2014.5.30)
特許権者または実用新案権者 【識別番号】504132272
【氏名又は名称】国立大学法人京都大学
発明者または考案者 【氏名】末永 幸平
【氏名】蓮尾 一郎
個別代理人の代理人 【識別番号】110000280、【氏名又は名称】特許業務法人サンクレスト国際特許事務所
審査官 【審査官】加舎 理紅子
参考文献・文献 特開2004-178300(JP,A)
特開2003-271679(JP,A)
山根智,ハイブリッドシステムの仕様記述言語と形式的検証手法,第48回 システム制御情報学会研究発表講演会講演論文集,2004年 5月21日,p.37-40
足立正和 他,同期型言語を用いたソフトウェア検証:クルーズコントロールシステムにおける事例紹介,コンピュータソフトウェア,日本ソフトウェア科学会,2006年 7月26日,VOL.23,NO.3,p.85-90
調査した分野 G06F 17/50
G06F 11/36
特許請求の範囲 【請求項1】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、
前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、
前記モデルのコードを、形式的検証を行うプログラム検証器によって検証することで、前記ハイブリッドシステムの検証を行う検証ステップと、
を含み、
前記プログラミング言語は、無限小を示す記号が導入されたプログラミング言語であり、
前記モデルは、前記ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされている
ハイブリッドシステムの検証方法。
【請求項2】
前記プログラム検証器は、定理証明器を含み、
前記検証ステップでは、前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項1記載のハイブリッドシステムの検証方法。
【請求項3】
前記検証ステップに先立って、前記モデルのコードにおける無限小を示す前記記号を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記モデルのコードを検証する
請求項1又は2記載のハイブリッドシステムの検証方法。
【請求項4】
前記検証ステップに先立って、前記検証条件を示す論理式における無限小を示す記号を、実数値を示す表現に置換する置換ステップを更に含み、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、
前記検証ステップでは、前記置換ステップによって置換された後の前記論理式を前記定理証明器によって証明する
請求項2記載のハイブリッドシステムの検証方法。
【請求項5】
前記数値を表す前記記号は、正の整数を示す記号である
請求項3又は4記載のハイブリッドシステムの検証方法。
【請求項6】
前記検証ステップに先立って、前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加ステップを更に含む
請求項1~5のいずれか1項に記載のハイブリッドシステムの検証方法。
【請求項7】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証装置であって、
前記ハイブリッドシステムの動作を、無限小を示す記号が導入されたプログラミング言語によってコーディングしたモデルの入力を受け付ける入力部と、
前記入力部によって受け付けた前記モデルのコードを記憶する記憶部と、
前記記憶部に記憶された前記モデルのコードに対して、形式的検証によって検証を行うプログラム検証器と、
前記プログラム検証器による検証結果を、前記ハイブリッドシステムの検証結果として出力する出力部と、
を備え、
前記モデルは、ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされているハイブリッドシステムの検証装置。
【請求項8】
前記プログラム検証器は、定理証明器を含み、
前記プログラム検証器は、前記記憶部に記憶された前記モデルのコードの検証条件を示す論理式を生成し、前記論理式を前記定理証明器によって証明することで、前記モデルのコードを検証する
請求項7記載のハイブリッドシステムの検証装置。
【請求項9】
前記記憶部に記憶されている前記モデルのコードにおける無限小を示す前記記号を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記モデルのコードを検証する
請求項7又は8記載のハイブリッドシステムの検証装置。
【請求項10】
前記検証条件を示す論理式における無限小を示す記号を、実数値を示す表現に置換する置換処理部を更に備え、
前記実数値を示す前記表現は、数値を表す記号を含み、前記数値の絶対値が増加するにつれて0に収束する値を示す表現であり、
前記プログラム検証器は、前記置換処理部によって置換された後の前記論理式を前記定理証明器によって証明する
請求項8記載のハイブリッドシステムの検証装置。
【請求項11】
前記数値を表す前記記号は、正の整数を示す記号である
請求項9又は10記載のハイブリッドシステムの検証装置。
【請求項12】
前記記憶部に記憶された前記モデルのコードに含まれているループに対して、ループ不変表明を付加する付加部を更に備える
請求項7~11のいずれか1項に記載のハイブリッドシステムの検証装置。
【請求項13】
コンピュータを、請求項7~12のいずれか1項に記載の検証装置として機能させるためのコンピュータプログラム。
【請求項14】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための方法であって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルをコンピュータにより生成する生成ステップを含み、
前記プログラミング言語は、無限小を示す記号が導入されたプログラミング言語であり、
前記生成ステップでは、前記ハイブリッドシステムにおける前記連続値の微小変化量を、無限小を示す前記記号を用いてコーディングしたコードが生成される
ハイブリッドシステムのモデル変換方法。
【請求項15】
連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムのブロック線図を、ハイブリッドシステムの検証用のモデルに変換するための装置あって、
前記ブロック線図が示す前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを生成する生成部を備え、
前記プログラミング言語は、無限小を示す記号が導入されたプログラミング言語であり、
前記生成部は、前記ハイブリッドシステムにおける前記連続値の微小変化量を、無限小を示す前記記号を用いてコーディングしたコードを生成する
ハイブリッドシステムのモデル変換装置。
【請求項16】
コンピュータを、請求項15記載のモデル変換装置として機能させるためのコンピュータプログラム。
【請求項17】
形式的検証を行うプログラム検証器によって前記形式的検証が行われるコードであって、
前記コードは、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの動作が、無限小を示す記号が導入されたプログラミング言語によってコーディングされたものであり、
前記コードでは、前記ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされている
コード。
発明の詳細な説明 【技術分野】
【0001】
本発明は、ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラムに関するものである。
【背景技術】
【0002】
ハイブリッドシステムは、制御理論における用語であり、速度や温度のような物理量を表す連続値と、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値とが相互に影響を及ぼしあってシステム全体が動作するのが特徴である。
【0003】
典型的なハイブリッドシステムとしては、自動車や航空機など、物理量の制御にソフトウェアが関わるようなシステムが挙げられる。例えば、自動車においては、モータの回転数、ブレーキオイルの圧力、内燃機関での燃焼量といった連続値と、ABSを動作させるかどうか等の離散値とが、時々刻々と変化しながら自動車の動作を実現している。
このため、ハイブリッドシステムは、連続値のみを扱うプラントや離散値のみを扱うソフトウェアとは異なった複雑さを持っている。
【0004】
ハイブリッドシステムを記述できるシステムとして、MathWorks社のSimulinkなどがある。
連続的な値のみを扱うシステムを対象とする従来の制御理論では、信号の流れを、図式を用いて表現する手法がよく用いられる。これを計算機上に実現し、さらに離散的な状態変化を表現するブロックを追加して拡張したのが、Simulinkなどの枠組みである。
【0005】
現在、ハイブリッドシステムの開発現場では、Simulinkなどの枠組みを利用して、ハイブリッドシステムの開発が行われている。
【先行技術文献】
【0006】

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

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

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

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

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

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

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

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

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

【0035】
[2. ハイブリッドシステムのモデリング言語]
本実施形態では、手続き型プログラミング言語のエッセンスであるwhile言語(Glynn Winskel. Formal Semantics of Programming Languages. The MIT Press, February 1993.)を、無限小の値を表すdtという記号で拡張した言語であるwhiledtを用いる。
無限小の値を言語に加えることにより、連続量を扱うシステムを、手続き型プログラミング言語で記述することができる。

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

【0037】
[2.1 モデリング言語whiledtの仕様]
以下に、本実施形態で用いられるwhiledt言語の定義の例を示す。
【数1】
JP0005843230B2_000002t.gif

【0038】
whiledt言語の定義は、BNF記法で記述されており、例えば、
a::=x|r|dt|a aop a
は、「aは、x,r,dtもしくはa aop aのいずれかである」という意味である。
aは、算術式で、変数、実数定数、無限小を表す記号dtか、算術演算(aop)のいずれかである。
bは、真偽値を表す式で、真を表す値、偽を表す値、ブール演算(and演算、or演算またはnot演算)または算術式間の関係式(a<a等)のいずれかである。

【0039】
cはコマンド(プログラムで実行される文)であり、それぞれの意味は以下の
通りである。
skip : なにも実行せずに終了する。
x:=a : 算術式aを評価し、その評価結果を変数xに代入する。
c1;c2 : コマンドcを実行し、その後コマンドcを実行する。
if b then c else c: 式bを評価し、その結果が真ならばcを実行し、偽ならばcを実行する。
while b do c done : 式bが真である間、cを繰り返し実行する。

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

【0041】
[2.2 whiledt言語によるプログラム例(モデル例)]
[例1]
初めに非常にシンプルなwhiledtのプログラム例を示す。このプログラムは微分方程式
【数2】
JP0005843230B2_000003t.gif

に従ったx(t)の時間発展を時刻5まで計算する。whileコマンドの各ループにおいて、xの値は微分方程式で指定された現時刻でのxの微小変化量(x×dt)だけ変化する。プログラム中のassert(x≧2)は、この時点においてx≧2が成り立たなければならないということを表しており、この条件が必ず成り立つことを、後述のプログラム論理を用いて検証する。

【0042】
【数3】
JP0005843230B2_000004t.gif

【0043】
[例2]
他の一例として先行研究(Andre Platzer.Differential dynamic logic for hybrid systems. J. Autom.Reasoning, 41(2):143-189, 2008.)にて取り上げられているヨーロッパ鉄道制御システム(ETCS)のモデルを挙げる。
accelは定数加速度aで時刻εまで加速する電車をモデル化している。
ここで変数vは電車の速度、変数zは電車の位置を表現している。whileループで時刻tを無限小量ずつ変化させ、コマンドCdrive内ではv:=v+a×dtで速度vを、加速度aに応じて変化させ、z:=z+v×dtで電車の位置zを現在の速度vに応じて変化させている。
【数4】
JP0005843230B2_000005t.gif

【0044】
また、以下のプログラムcchkAndBrakeは、電車の位置を時間間隔εでモニタリングし、現在の位置が点mより距離sを越えていることを検知すると加速度を-bに変化させ減速し停車する電車をモデル化している。
【数5】
JP0005843230B2_000006t.gif

【0045】
[例3]
別の現実に近い例として、先行研究(Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, pages 209-229, 1992.)にて取り上げられている貯水槽モニタのモデルを挙げる。
図2に示すように、この貯水槽100には給水口101と排水口102が付いており、給水口101のバルブ103が開いているときは水位が毎秒1cmで上昇し、バルブ103が閉じているときには毎秒2cmで下降する。バルブ103の操作はスイッチ104で行われており、バルブ103の開閉はスイッチ104の操作後2秒経ってから起こる。

【0046】
この貯水槽をモデル化したのが以下のプログラムcwaterである。変数yは水位を、変数xはスイッチ操作からの変化時間を、sはスイッチの状態(1=on,0=off)を、vはバルブ103の状態(1=開,0=閉)を表している。
以下のプログラムにおいて、case{・・・}は、初めから順番に条件を検査し、条件が成り立った部分のプログラムを実行する構文である。
【数6】
JP0005843230B2_000007t.gif

【0047】
[3.検証装置(プログラム論理を用いた検証アルゴリズム)]
whiledt言語によってコーディングされたハイブリッドシステムのモデルは、プログラミング言語的に記述されているため、形式的検証を行うプログラム検証器45によって検証が可能である。

【0048】
図1に示すように、検証装置4は、whiledt言語によってコーディングされたハイブリッドシステムのモデルのコード(プログラム)の入力を受け付ける入力部41を備えている。入力部41は、システム1内部の他の機能(例えば、図1の変換器3)から、コードの入力を受け付けても良いし、システム1の外部からコードの入力を受け付けても良い。

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

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

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

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

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

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

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

【0056】
[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とが、(無限小の値を含まない)実数上のプログラムc・論理式Qに変換される。セクション化により、無限小値を含むプログラムの検証に無限小値を対象としない既存手法(例えば、以下で述べるループ不変表明の計算等)を適用することが可能となる。

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

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

【0058】
この例について、セクション化(置換ステップ)の結果得られるプログラムcと論理式Qは、次のようになる。
【数8】
JP0005843230B2_000009t.gif

【0059】
[3.2 ループ不変表明の計算]
前記付加ステップでは、ループ不変表明計算部44が、セクション化して得られたプログラムcについてループ不変表明(loop invariant assertion)を計算し、プログラムcに付加する。

【0060】
ループ不変表明とは、プログラム中のループが、要求される仕様を満たしているか否かを検証するための論理式である。ループ不変表明は、セクション化されたプログラムc中のループ文において、ループの入口と出口で必ず成り立っているべき論理式として記述される。ループ不変表明計算部44は、ループ不変表明を構成する論理式を、自動的に生成して、プログラムc中に付加する。
ループ不変表明を自動生成するアルゴリズムとしては、例えば、Sriram Sankaranarayanan、 Henny B. Sipma, and Zohar Manna. Nonlinear loop invariant generation using groebner bases. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’04, pages 318-329, New York, NY, USA,2004. ACM.に開示されているものを利用することができる。ループ不変表明の計算・付加は、手動で行っても良い。

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

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

をとることができる。

【0063】
すなわち、ループの入口と出口において、必ずt=n/iとx=(1+1/i)が成り立つような0以上のnが存在する。実際に、c中のwhile文においては初めてループに入る時にはx=1かつt=0が成り立っているので、nとして0を取ればループ不変表明は成り立つ。また、ループの入口でループ不変表明が成り立っているときにループ本体を一回実行すると、tの値は1/iだけ増加し、xの値は、(1+1/i)倍されるので、上記の論理式のnをn+1と取り直せば、やはりループの出口でもループ不変表明が成り立っている。

【0064】
[3.3 検証条件の生成]
プログラム検証器45の検証条件生成器46は、記憶部42に記憶されたプログラム(セクション化され、ループ不変表明が付加されたプログラム)c、及び事前条件(セクション化された事前条件)Qについて、検証条件の生成という手続きを行う。

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

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

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

【0068】
検証条件生成アルゴリズムVCでは、プログラムc(セクション化され、ループ不変表明が付加されたプログラム)と、事前条件Qを受け取り、検証条件を生成する。
アルゴリズムVCは、再帰関数VCを用いて定義されている。
VC(c,Q)は、プログラムcの実行後に、Qが成り立つために、cの実行前に成り立っているべき条件を返す。
例えば、VC(c;c,Q)の定義は、「VC(c,Q)の結果をQ’’、VC(c,Q’’)の結果をQ’としたときに、全体の結果はQ’である」のように読む。
VCは、「VCによって返された条件が、事前条件から帰結される」ことを意味する論理式を検証条件として返す。
なお、検証条件生成アルゴリズムにおいて、Q[x->a]は、Q中の変数xをaで置き換える操作を示す。

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

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

なお、Q’’(t,x,i)は、ループ不変表明計算部44によって計算されたループ不変表明である。

【0071】
[3.4 定理証明器を用いた検証条件の証明]
前述のように生成された検証条件が、「有限個のiを除いて正しい」ことが示されれば、元のwhiledtのプログラムcは、与えられた性質を必ず満たす。この検証条件(論理式)の証明のため、本実施形態では、定理証明器(Theorem Prover)47を用いる。プログラム検証の分野においては、与えられた論理式が成り立つかどうかを自動的に判定する手法(Beheads Akbarpour and L. C. Paulson. Metitarski: An automatic theorem prover for real-valued special functions. J. Automated Reasoning,44(3):175-205, 2010.)や、一部人間の支援によって判定する手法(The Coq Development Team. Reference Manual - The Coq Proof Assistant.INRIA, 2010. http://coq.inria.fr/refan/.)が知られており、これらの手法を用いて検証条件が成り立つかどうかを判定する。

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

と書ける。

【0073】
したがって、この論理式を定理証明器で証明することによって、元のプログラム中のassert(Q)が必ず成り立つことが検証できる。
例1のプログラムについての検証条件を整理すると、
【数13】
JP0005843230B2_000014t.gif
が成り立てば、検証条件が成り立つことが分かる。
したがって、定理証明器47で証明すべき論理式は、
【数14】
JP0005843230B2_000015t.gif

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

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

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

【0076】
[4.検証例]
[4.1 whiledtのプログラムの例A]
whiledtによってハイブリッドシステムの動作をコーディングしたモデルのプログラムコードAを、以下に示す。なお、以下のコードにおいて、「&&」は、論理積を示す論理演算子である。
【数15】
JP0005843230B2_000016t.gif

【0077】
[4.2 セクション化]
例Aのコードをセクション化したコードA1を、以下に示す。セクション化により、例Aのコードに含まれていたdt(無限小を表す記号)が、”1/i”に変換され、無限小dtを含まない形となっている。したがって、既存のソフトウェア検証手法を適用することが可能となっている。
【数16】
JP0005843230B2_000017t.gif

【0078】
[4.3 ループ不変表明の付加]
セクション化されたコードA1に、ループ不変表明を付加したコードA2を、以下に示す。
【数17】
JP0005843230B2_000018t.gif

【0079】
[4.4 検証条件]
セクション化され、かつ、ループ不変表面が付加されたコードA2に対し、事前条件をtrueとして、検証条件生成アルゴリズムVCを適用して得られる検証条件を、以下に示す。この検証条件は、定理証明器Coq(http://coq.inria.fr/refan/)で扱えるフォーマットで記述されている。なお、実際に定理証明器で証明すべき論理式は、以下に示す論理式の先頭に、「exists n:nat,i>n ->」を付加したものになる。
【数18】
JP0005843230B2_000019t.gif

【0080】
[4.5 セクション化せずにループ不変表明を付加]
例AのコードAを、セクション化せずにループ不変表明を付加したコードA3を、以下に示す。
【数19】
JP0005843230B2_000020t.gif

【0081】
[4.6 セクション化せずに生成された検証条件]
セクション化せずにループ不変表明を付加したコードA3に対し、事前条件をtrueとして、検証条件生成アルゴリズムVCを適用して得られる検証条件を、以下に示す。
無限小を直接扱える定理証明器を用いれば、この検証条件の証明を行うことで、コードAの安全性を示すことができる。無限小を扱える定理証明器としては、(Tania Bedrax-Weiss and Rolando Chuaqui, INFMAL: An Infinitesimal Analysis Interactive Theorem Prover and Problem Solver. Proceedings of the XII International Conference of the Chilean Computer Science Society, Santiago, Chile, October 1992.)に記載のものがある。以下の検証条件中のdtを”1/i”で置き換えたものは、[4.4 検証条件]で示した検証条件と一致する。
【数20】
JP0005843230B2_000021t.gif

【0082】
[5.whiledtプログラムへの変換]
図3は、図1に示す変換装置3におけるモデル変換処理を示している。図1に示すように、変換装置3は、生成部3aと、変換テーブル3bと、を備えている。
生成部3aは、コンピュータ支援設計システム2によって生成されたハイブリッドシステムのブロック線図(モデル)から、whiledt言語でコーディングされたプログラム(ハイブリッドシステムのモデルのコード)を生成する。
変換テーブル3bは、ハイブリッドシステムのブロック線図から、whiledt言語のプログラムコードに生成するために、生成部3aによって参照される。

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

【0084】
図4は、コンピュータ支援設計システム2によって生成されたハイブリッドシステムのブロック線図の例を示している。このブロック線図は、時刻1で値が0から1になるステップ信号を生成して出力するブロック51、入力信号の加減算を行って出力するブロック52、入力信号を増幅して出力するブロック53a,53b,53c、入力信号の積分をして出力するブロック54a,54b等の各種ブロックを備えている。各ブロックは、結線L1~L7によって適宜接続されている。

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

【0086】
変換装置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’を示している。

【0087】
さらに、生成部3aは、時間を表す変数tを生成する(ステップS4)。
続いて、生成部3aは、ステップS2~4で生成した各変数xi,xi’,si,si’,tを初期化するコードc0を生成する(ステップS5)。以下は、各変数を0で初期化したコードc0の例を示している。
【数21】
JP0005843230B2_000022t.gif

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

【0089】
さらに続けて、生成部3aは、無限小時間後の各変数xi,xi’,si,si’の値を計算して変数を更新するためのコードc1を生成する(ステップS6)。コードc1は、コードc11と、コードc12とからなる。

【0090】
コードc11は、各ブロックにおける無限小時間後の出力値として、変数xiに基づいて計算される値を、xi’に代入するコードである(ここでは、xiのiと、xi’のiとは、一般には異なる値である)。
生成部3aは、ブロック線図中の各ブロックについて、変換テーブル3bを参照することで、コードc11を生成する(ステップS6a)。なお、変換テーブル3bは、変換装置3を構成するコンピュータ又はその他の装置の記憶部に記憶されている。

【0091】
図6は、ブロック線図において用いられるブロックと、ブロックに対応するwhiledt言語のコードとの対応を規定した変換テーブルの例を示している。なお、図6では、ブロック線図に用いられるブロックとして、Simulinkで用いられるブロックの一部を例として挙げた。
図6の変換テーブル3bの左側が、Simulinkにおいて用いられるブロックを示しており、変換テーブル3bの右側が、各ブロックに対応するwhiledt言語のコードを示している。

【0092】
生成部3aが、コードc11を生成する際には、変換テーブル3b中のwhiledt言語のコードにおける変数を示す記号のうち、xi,xi’,xjは、変換対象のブロックの入力又は出力に接続された結線に割り当てられた変数名に置換される。また、変換テーブル3b中のwhiledt言語のコードにおける変数を示す記号のうち、si,si’は、置換対象のブロックに割り当てられた状態変数名に置換される。
また、変換テーブル3b中のwhiledt言語のコードにおけるその他の変数を示す記号(dtを除く)は、置換対象のブロックに設定されたパラメータ(ブロック線図のデータ中のパラメータ)が示す値に置換される。

【0093】
生成部3aが、図5に示すブロック線図に関して、変換テーブル3bを参照することで生成したコードc11を以下に示す。
【数22】
JP0005843230B2_000023t.gif

【0094】
コードc12は、xi’,si’の値を、xi,siに代入するコードである(ここでは、xiのiと、xi’のiとは同じ値であり、siのiと、si’のiも同じ値である)。
生成部3aが、図5に示すブロック線図に関して、xi’,si’の値を、xi,siに代入するコードとして生成したコードc12を以下に示す。
【数23】
JP0005843230B2_000024t.gif

【0095】
さらに、生成部3aは、無限小を示す記号dtを用いて、時間を示す変数tを更新するコード(while文)を生成し、先に生成したコードc0及びコードc1を組み合わせて、図5に示すハイブリッドシステムのブロック線図全体の動作を示すコード[c0; while (t<1/dt) {c1;t:=t+dt}]を生成する。

【0096】
生成されたコードは、[c0; while (t<1/dt) {c1;t:=t+dt}]は、コンピュータの記憶部に記憶されて、検証装置4による検証に用いても良いし、表示装置などに出力されてもよい。

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

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

【0099】
[6.付記]
なお、上記において開示した事項は、例示であって、本発明を限定するものではなく、様々な変形が可能である。
【符号の説明】
【0100】
1 システム
2 コンピュータ支援設計システム
3 変換装置
3a 生成部
3b 変換テーブル
4 検証装置
41 入力部
42 記憶部
43 セクション化部(置換処理部)
44 ループ不変表明計算部
45 プログラム検証器
46 検証条件生成器
47 定理証明器
48 出力部
図面
【図1】
0
【図2】
1
【図3】
2
【図4】
3
【図5】
4
【図6】
5