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

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

国内特許コード P130008485
整理番号 S2011-0785-N0
掲載日 2013年1月17日
出願番号 特願2011-135201
公開番号 特開2013-003897
登録番号 特許第5843230号
出願日 平成23年6月17日(2011.6.17)
公開日 平成25年1月7日(2013.1.7)
登録日 平成27年11月27日(2015.11.27)
発明者
  • 末永 幸平
  • 蓮尾 一郎
出願人
  • 国立大学法人京都大学
発明の名称 ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム 新技術説明会
発明の概要 【課題】ハイブリッドシステムの検証を、ソフトウェア検証の手法で行えるようにする。
【解決手段】 連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの検証方法であって、前記ハイブリッドシステムの動作を、プログラミング言語によってコーディングしたモデルを作成する作成ステップと、モデルのコードを、形式的検証を行うプログラム検証器45によって検証することで、ハイブリッドシステムの検証を行う検証ステップと、を含んでいる。プログラミング言語は、無限小を記述可能なプログラミング言語である。モデルは、ハイブリッドシステムにおける連続値の変化が、前記無限小を用いてコーディングされている。
【選択図】図1
従来技術、競合技術の概要


ハイブリッドシステムは、制御理論における用語であり、速度や温度のような物理量を表す連続値と、レジスタの値やメモリアドレスのようなソフトウェアの動作に関わる離散値とが相互に影響を及ぼしあってシステム全体が動作するのが特徴である。



典型的なハイブリッドシステムとしては、自動車や航空機など、物理量の制御にソフトウェアが関わるようなシステムが挙げられる。例えば、自動車においては、モータの回転数、ブレーキオイルの圧力、内燃機関での燃焼量といった連続値と、ABSを動作させるかどうか等の離散値とが、時々刻々と変化しながら自動車の動作を実現している。
このため、ハイブリッドシステムは、連続値のみを扱うプラントや離散値のみを扱うソフトウェアとは異なった複雑さを持っている。



ハイブリッドシステムを記述できるシステムとして、MathWorks社のSimulinkなどがある。
連続的な値のみを扱うシステムを対象とする従来の制御理論では、信号の流れを、図式を用いて表現する手法がよく用いられる。これを計算機上に実現し、さらに離散的な状態変化を表現するブロックを追加して拡張したのが、Simulinkなどの枠組みである。



現在、ハイブリッドシステムの開発現場では、Simulinkなどの枠組みを利用して、ハイブリッドシステムの開発が行われている。

産業上の利用分野


本発明は、ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラムに関するものである。

特許請求の範囲 【請求項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】
形式的検証を行うプログラム検証器によって前記形式的検証が行われるコードであって、
前記コードは、連続値と離散値とが相互に影響を与えながら動作するハイブリッドシステムの動作が、無限小を示す記号が導入されたプログラミング言語によってコーディングされたものであり、
前記コードでは、前記ハイブリッドシステムにおける前記連続値の微小変化量が、無限小を示す前記記号を用いてコーディングされている
コード。
産業区分
  • 演算制御装置
  • 記憶装置
  • 入出力装置
  • 計算機応用
  • その他情報処理
国際特許分類(IPC)
Fターム
画像

※ 画像をクリックすると拡大します。

JP2011135201thum.jpg
出願権利状態 登録
ライセンスをご希望の方、特許の内容に興味を持たれた方は、下記までご連絡ください。


PAGE TOP

close
close
close
close
close
close
close