形式手法を用いたシステム設計検証技術

• Item type: SIG Technical Reports(1)
• 公開日: 2010-03-11
• タイトル: 形式手法を用いたシステム設計検証技術
• タイトル / 言語: en
• タイトル: Using Formal Methods for System Design Verification Technology
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 検証・Web
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 三菱電機（株）情報技術総合研究所
• 著者所属: 三菱電機（株）情報技術総合研究所
• 著者所属: 三菱電機（株）情報技術総合研究所
• 著者所属: 三菱電機（株）情報技術総合研究所
• 著者所属(英): en
• 著者所属(英): Information Technology R&D Center, Mitsubishi Electric Corporation
• 著者所属(英): en
• 著者所属(英): Information Technology R&D Center, Mitsubishi Electric Corporation
• 著者所属(英): en
• 著者所属(英): Information Technology R&D Center, Mitsubishi Electric Corporation
• 著者所属(英): en
• 著者所属(英): Information Technology R&D Center, Mitsubishi Electric Corporation
• 著者名: 市原, 利浩; 上野, 浩一郎; 磯田, 誠; 大貫, 智洋
• 著者名(英): Toshihiro, Ichihara; Ueno, Koichiro; Makoto, Isoda; Tomohiro, Onuki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: ソフトウェア・システムの大規模化・高機能化に伴い，従来の人手によるレビューやテストの実践だけでは，設計で混入した不具合を完全に除去することが難しくなっている．そのため，近年，形式手法の一つであるモデル検査による検証技術が注目を集めている．しかし，モデル検査技術を広く展開するには，現場の開発者にとってモデル検査ツールに与える仕様モデルの定義や出力される結果の解析が困難という課題がある．これに対して我々は，特定の分野に特化した記法を用いて仕様モデルを定義することで，仕様モデル定義の負荷の軽減を狙うこと，モデル検査器が出力した検証結果をモデル変換することで，開発者にとって解析しやすいモデルの出力を実施するモデル検査器フロントエンドを適用することを検討している．本稿では，このアプローチによるシステム設計検証技術について報告する
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: While software systems become larger and more complex, the verification of the software systems' specification becomes harder. In recent, therefore, model checking technology is focused as a method to extract defects of designed specifications in such large software intensive systems. However, for those practical software developers, it is hard to rewirte their specifications for model checking tools, and also hard to understand the output of the checkers. In this paper, we propose an approach to overcome these issues by combining 2 approaches: Domain-oriented modeling language, and Model Conversion between ordinal UML and Model checking tools. Domain-oriented modeling language helps developers to specify their systems more easily, and Model Conversion mechanism helps those developers to understand the result of those model checking tools on their own domain-oriented modeling languages. We are now developing the method and supporting tools for our model checking method.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2010-SE-167, 号 32, p. 1-8, 発行日 2010-03-11
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会