CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 28: システムLSI仕様の形式化と検証項目自動生成


実施年度2007
概要 システムLSI仕様書を形式化し、それから検証項目を自動生成した
担当者 安部達也、岡本圭史、齋藤正也、武山誠
班名 フィールドワーク7班
寄与 株式会社ルネサステクノロジ
関連する事例

題材

領域 システムLSI
題材の詳細
ルネサステクノロジ社製CPU命令仕様書
形態 仕様書
言語 自然言語、C言語風言語
規模 90命令程度
題材の情報源 ルネサステクノロジ社製CPU命令仕様書(公開予定)

検証のデータ

目的
仕様書の形式化及び検証項目の自動生成
検証内容
(非公開)
結果
仕様書中の代表的命令の形式化終了、検証項目自動生成ツール試作終了
検証手法 形式的モデルからのテストケース自動生成
モデル化法 仕様書及びエンジニアの知識から手動で形式化
使用ツール Agda2
スケジュール、
労力、時間など
エンジニア(二名)、研究者(四名)が5ヶ月間従事
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 The 20th IFIP Int. Conference on Testing of Communicating Systems (TESTCOM) and the 8th Int. Workshop on Formal Approaches to Testing of Software (FATES), "Formalization of System LSI Specification and Automatic Generation of Verification Items", Tatsuya Abe, Takashi Higuchi, Rintaro Imai, Yoshiki Kinoshita, Satoshi Nakano, Keishi Okamoto, Masaya Saito, Makoto Takeyama, 2008年6月13日
知的財産
その他

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