Top > Search of Japanese Patents > VERIFICATION METHOD, VERIFICATION DEVICE, AND VERIFICATION COMPUTER PROGRAM FOR HYBRID SYSTEM; AND MODEL CONVERSION METHOD, MODEL CONVERSION DEVICE, AND MODEL CONVERSION COMPUTER PROGRAM FOR HYBRID SYSTEM

VERIFICATION METHOD, VERIFICATION DEVICE, AND VERIFICATION COMPUTER PROGRAM FOR HYBRID SYSTEM; AND MODEL CONVERSION METHOD, MODEL CONVERSION DEVICE, AND MODEL CONVERSION COMPUTER PROGRAM FOR HYBRID SYSTEM UPDATE_EN meetings

Patent code P130008485
File No. S2011-0785-N0
Posted date Jan 17, 2013
Application number P2011-135201
Publication number P2013-003897A
Patent number P5843230
Date of filing Jun 17, 2011
Date of publication of application Jan 7, 2013
Date of registration Nov 27, 2015
Inventor
  • (In Japanese)末永 幸平
  • (In Japanese)蓮尾 一郎
Applicant
  • (In Japanese)国立大学法人京都大学
Title VERIFICATION METHOD, VERIFICATION DEVICE, AND VERIFICATION COMPUTER PROGRAM FOR HYBRID SYSTEM; AND MODEL CONVERSION METHOD, MODEL CONVERSION DEVICE, AND MODEL CONVERSION COMPUTER PROGRAM FOR HYBRID SYSTEM UPDATE_EN meetings
Abstract PROBLEM TO BE SOLVED: To verify a hybrid system by a technique for software verification.
SOLUTION: There is provided a verification method for a hybrid system in which a continuous value and a discrete value operate while affecting each other, the verification method including a generation step of generating a model by coding the operation of the hybrid system with a program language, and a verification step of verifying the hybrid system by verifying the code of the model by a program verifier 45 which performs format verification. The program language is a program language in which an infinitesimal can be described. The model has variation in the continuous value of the hybrid system coded using the infinitesimal.
Outline of related art and contending technology (In Japanese)

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

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

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

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

Field of industrial application (In Japanese)

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

Scope of claims (In Japanese)
【請求項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(International Patent Classification)
F-term
Drawing

※Click image to enlarge.

JP2011135201thum.jpg
State of application right Registered
Please contact us by e-mail or facsimile if you have any interests on this patent. Thanks.


PAGE TOP

close
close
close
close
close
close
close