TOP > 国内特許検索 > 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 NEW

国内特許コード P180015679
整理番号 5295
掲載日 2018年11月22日
出願番号 特願2016-017441
公開番号 特開2017-138679
出願日 平成28年2月1日(2016.2.1)
公開日 平成29年8月10日(2017.8.10)
発明者
  • 末永 幸平
  • 樹下 稔
  • 小島 健介
出願人
  • 国立大学法人京都大学
発明の名称 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 NEW
発明の概要 【課題】不変条件を生成するための新たな技術を提供する。
【解決手段】不変条件生成装置100は、プログラムコードが記憶される記憶部300と、不変条件を生成する処理を実行する処理部200を備える。処理部200は、不変条件を生成する第3処理を実行する。第3処理は、プログラムコードが実行されることによる1又は複数の部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、表現行列の固有値と固有ベクトルを求める演算処理と、固有値及び固有ベクトルの組と、1又は複数の部分式と、に基づいて、不変条件を生成する不変条件生成処理と、を含む。
【選択図】図1
従来技術、競合技術の概要


不変条件(Invariant)は、プログラムコード(以下、単に「コード」ということがある)の形式的検証(formal verification)に用いられる。形式的検証は、プログラムコードの正当性を数学的な形式的手法で証明することである。プログラムコードに含まれるある処理に対する不変条件は、その処理の実行前後において成立する条件として構成される。while文のようなループ処理に対する不変条件は、ループ不変条件(Loop Invariant)と呼ばれる。ループ不変条件は、ループの開始時点で成立するとともに、ループを何回繰り返しても成立する条件として構成される。



不変条件を生成する従来の方法には、非特許文献1等に記載のテンプレート法(template-based method)がある。テンプレート法では、多項式pが、不変条件に関係するテンプレートとして生成される。多項式pは、検証対象のプログラムコードに含まれるシンボルと不定係数によって構成される。シンボルとは、プログラムに含まれる変数又は定数を示す文字又は記号である。そして、p=0が不変条件であるような制約が生成される。この制約を解析することで、不変条件が得られる。

産業上の利用分野


本発明は、不変条件生成装置等に関するものである。

特許請求の範囲 【請求項1】
不変条件生成装置であって、
プログラムコードが記憶される記憶部と、
前記不変条件を生成する処理を実行する処理部を備え、
前記処理は、
前記記憶部から前記プログラムコードを読み出す第1処理と、
多項式を構成するための1又は複数の部分式を生成する第2処理と、
前記不変条件を生成する第3処理と、
を含み、
前記第3処理は、
前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、
前記表現行列の固有値と固有ベクトルを求める演算処理と、
前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記不変条件を生成する不変条件生成処理と、
を含む
不変条件生成装置。

【請求項2】
前記表現行列の一つの固有値に対して複数の独立な固有ベクトルが存在する場合には、
前記不変条件生成処理は、複数の固有ベクトルの線形結合を、前記不変条件の生成に用いる
請求項1記載の不変条件生成装置。

【請求項3】
1又は複数の前記部分式それぞれの前記変換が、前記変換行列だけでなく余りベクトルによっても表される場合には、
前記不変条件生成処理は、前記固有ベクトルと前記余りベクトルとの内積が0になる条件の下で前記不変条件を生成する
請求項1又は2記載の不変条件生成装置。

【請求項4】
請求項1~3のいずれか1項に記載の不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラム。

【請求項5】
不変条件を生成する処理を実行する処理部によって実行される方法であって、
記憶部からプログラムコードを読み出す第1処理を実行すること、
多項式を構成するための1又は複数の部分式を生成する第2処理を実行すること、
前記不変条件を生成する第3処理を実行すること、
を含み、
前記第3処理は、
前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、
前記表現行列の固有値と固有ベクトルを求める演算処理と、
前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記ループ不変条件を生成する不変条件生成処理と、
を含む
方法。

【請求項6】
プログラムコードを作成すること、
請求項5に記載の前記記憶部が、作成されたプログラムコードを記憶すること、
請求項5に記載の方法によって、前記プログラムコードの不変条件を生成すること、
前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、
前記形式的検証の結果に基づいて前記プログラムコードを修正すること、
を含むプログラムコードの製造方法。
国際特許分類(IPC)
Fターム
画像

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

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


PAGE TOP

close
close
close
close
close
close
close