CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 23: Java の例外処理のSPIN による検証


実施年度2005
概要 Java プログラムの例外処理の整合性をモデル検査器SPIN を用いて検証する. Java プログラムでは,発生する例外と例外処理ブロックの内容に不整合が生じ る可能性がある.本実験では,この不整合を発見するためにモデル検査器SPIN と、例外解析器Jex を組み合わせる手法を開発.Jex はJava のプログラム とJava の標準ライブラリを入力とし、そのプログラムが実行時に発生しうる例 外を列挙する.これにより,検証対象のプログラムだけでなく,ライブラリを 起因とする例外処理をモデル化することができる.
担当者 斎藤正也, 高井利憲, 池上大介
班名 フィールドワーク3班
寄与 株式会社イシダ
関連する事例

題材

領域 Java で記述された通信プロトコル
題材の詳細
Java で記述されたサーバとC言語などで記述されたクライアントからなる
通信プロトコル.
形態 ソースコード
言語 Java
規模
題材の情報源

検証のデータ

目的


検証内容
(1) 例外処理の書き忘れ
(2) 起こりえない例外処理の記述
結果
既知のバグの再発見に成功
検証手法 モデル検査
モデル化法 (1) Java のプログラムから例外処理のフローのみを抜きだし、 Promela で記述されたモデルの概形を自動生成する (2) Java のプログラムをJex で解析した結果(プロ グラムが発生しうる例外のリスト) を(1) で作成し たPromela モデルに埋め込む(3) 検証のための時相 論理式を作成し、(2) でできあがったPromela モデ ルとともにSPIN に与えてモデル検査を行う。
使用ツール Spin, Jex
スケジュール、
労力、時間など
3人で二ヶ月ぐらい(?)
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
Java の例外処理のSPIN による検証, 斎藤正也, 高井利憲, 池上大介, 第三回システム検証の科学技術シンポジウム予稿集, 算譜科学研究速報, PS-2006-012, 15-18, http://unit.aist.go.jp/cvs/tr-data/PS06-012.pdf
論文発表
口頭発表 斎藤正也、高井利憲、池上大介: "Javaの例外処理のSPINによる検証", 第三 回システム検証の科学技術シンポジウム,豊中,2006年10月.
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.