Pat

J-GLOBAL ID：200903039467392629

ソースコード検証装置、及びソースコード検証方法

Inventor： 小泉 健 ,  小崎 光義
Applicant, Patent owner： 日本電気株式会社
Agent (1)： 工藤 実
Gazette classification：公開公報
Application number (International application number)：2008054863
Publication number (International publication number)：2009211503
Application date： Mar. 05, 2008
Publication date： Sep. 17, 2009
Summary：

【課題】ソースコードの検証に対してモデル検査を行う際に問題となる状態爆発を抑制する。【解決手段】ソースコード検証システム200は、検証対象ソースコード100をKripke構造モデル300に変換し、Kripke構造モデル300に対してモデル検査を行うことにより、検証対象ソースコード100を検証する。Kripke構造モデル300は、検証対象ソースコード100について定義された契約情報に記述された条件を満足しない状態を排除するようにKripke構造モデル300を生成する。【選択図】図1

Claim (excerpt)：

ソースコードを状態遷移モデルに変換する状態遷移モデル変換手段と、 前記状態遷移モデルに対してモデル検査を行うことにより、前記ソースコードを検証する検証手段 とを具備し、 前記状態遷移モデル変換手段は、前記ソースコードについて定義された契約情報に記述された条件を満足しない状態を排除するように前記状態遷移モデルを生成する ソースコード検証装置。

IPC (1)：

G06F 11/36

FI (1)：

G06F9/06 620M

F-Term (1)：

5B176EC02

Patent cited by the Patent：

Cited by applicant (4)

• プロパティ検証方法および装置
  Gazette classification：公開公報   Application number：特願平8-220005   Applicant：富士通株式会社
• 仕様書確認方法、仕様書確認プログラム、該プログラムを記録した記録媒体、および仕様書確認装置
  Gazette classification：公開公報   Application number：特願2005-147247   Applicant：富士通株式会社
• ソフトウェア試験支援装置
  Gazette classification：公開公報   Application number：特願2004-133732   Applicant：三菱電機株式会社
• ソフトウェアコンポーネントテストシステム及びソフトウェアコンポーネントテスト方法
  Gazette classification：公開公報   Application number：特願2004-272672   Applicant：富士ゼロックス株式会社

Cited by examiner (1)

• プロパティ検証方法および装置
  Gazette classification：公開公報   Application number：特願平8-220005   Applicant：富士通株式会社

Article cited by the Patent：

Cited by examiner (2)

• “形式手法によるC言語検証ツール「VARVEL」”
• “Cプログラム・モデル検査におけるDbC”