組込みソフトウェアの制御機構に対するモデル検査の適用に関する評価実験

• Item type: Symposium(1)
• 公開日: 2009-10-19
• タイトル: 組込みソフトウェアの制御機構に対するモデル検査の適用に関する評価実験
• タイトル / 言語: en
• タイトル: An Evaluation of Application of Model-Checking to ConrtolMechanizm of Embedded Software
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: セキュリティプロトコル・検証
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: (株) 三菱総合研究所
• 著者所属: 国立情報学研究所
• 著者所属: 株式会社NTTデータ
• 著者所属: 日立ソフトウェアエンジニアリング
• 著者所属(英): en
• 著者所属(英): Mitsubishi Research Institute,Inc.
• 著者所属(英): en
• 著者所属(英): National Institute of Informatics
• 著者所属(英): en
• 著者所属(英): NTT Data Corporation
• 著者所属(英): en
• 著者所属(英): Hitachi Software Engineering
• 著者名: 石黒, 正揮; 中島, 震; 梅村, 晃広; 田中, 一之
• 著者名(英): Masaki, Ishiguro; Shin, Nakajima; Akihiro, Umemura; Kazuyuki, Tanaka
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 製品化されるブルーレイディスクのモード制御機構に対してモデル検査システム SPIN を適用し、モード状態の整合性に関する検証を行った。モデル検査により、従来のテストケースによる方法では発見が困難な不具合を発見した。検証対象の形式モデリング、検証性質の記述および不具合箇所の特定についてまとめる。また、形式手法の導入によるコストと効果に関する評価結果を示す。
• 論文抄録(英) / 内容記述タイプ: Other
• 書誌情報: コンピュータセキュリティシンポジウム2009 (CSS2009) 論文集; 巻 2009, p. 1-6, 発行日 2011-10-12
• 出版者 / 言語: ja
• 出版者: 情報処理学会