| 講演名 | 2010-08-05 モバイルFeliCa ICチップ開発におけるSPINを用いたモデル検査による品質確保 只野 賢二, 栗田 太郎, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | モバイルFeliCa ICチップのファームウェアの品質向上手法として,モデル検査器であるSPINを用いて,C言語で記述したソースコードの検査を行った.本稿では,検査プロセス,検査モデルの設計・実装の方法,検査の成果に加えて,モデル検査手法の学習方法,導入の有効性,課題および今後の展望を報告する. |
| 抄録(英) | We applied SPIN model checker to C source code as a quality assurance method for Mobile FeliCa IC chip firmware. In this paper, we explain testing process, design and implementation method of test model, and test result. Also, innovation method of Model-checking, its validity, current challenge and future prospect is reported based on it. |
| キーワード(和) | モデル検査 / 組みこみ / Promela / SPIN |
| キーワード(英) | model checking / embedded software / Promela / SPIN |
| 資料番号 | SS2010-21 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2010/7/29(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モバイルFeliCa ICチップ開発におけるSPINを用いたモデル検査による品質確保 |
| サブタイトル（和） | |
| タイトル（英） | Quality Assurance by Using SPIN Model Checker in Mobile FeliCa IC Chip Development |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | 組みこみ / embedded software |
| キーワード(3)（和/英） | Promela / Promela |
| キーワード(4)（和/英） | SPIN / SPIN |
| 第 1 著者 氏名（和/英） | 只野 賢二 / Kenji TADANO |
| 第 1 著者 所属（和/英） | フェリカネットワークス株式会社 FeliCa Networks, inc. |
| 第 2 著者 氏名（和/英） | 栗田 太郎 / Taro KURITA |
| 第 2 著者 所属（和/英） | フェリカネットワークス株式会社 FeliCa Networks, inc. |
| 発表年月日 | 2010-08-05 |
| 資料番号 | SS2010-21 |
| 巻番号（vol） | vol.110 |
| 号番号（no） | 169 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |