状態遷移図の同期モデルへの詳細化および検証手法

• Item type: SIG Technical Reports(1)
• 公開日: 2010-11-04
• タイトル: 状態遷移図の同期モデルへの詳細化および検証手法
• タイトル / 言語: en
• タイトル: A Proposition of Refinement and Verification Method from Requirements to A Synchronous State Machine Model
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 設計検証
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 九州大学大学院システム情報科学研究院
• 著者所属: 九州大学大学院システム情報科学府
• 著者所属: 九州大学大学院システム情報科学研究院
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electric Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electric Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electric Engineering, Kyushu University
• 著者名: 大森, 洋一; 園田, 貴大; 荒木, 啓二郎
• 著者名(英): Yoichi, Omori; Takahiro, Sonoda; Keijiro, Araki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 計算機システムの社会基盤への浸透とそれらにおけるソフトウェアの役割が増すに従い，設計段階での信頼性向上が重要な課題となっている．フォーマルメソッドは，ソフトウェアの信頼性向上手法として長い歴史をもち，さまざまな論理に基づくモデル化に関する研究がなされている．本稿では，要求段階における抽象度の高い機能を対象とした制約を，フォーマルメソッドを用いた明示的な仕様として抽出し，主に時間に関する性質について，設計段階における状態機械のふるまいに関してそれらの仕様を検証する手法を提案する．本手法は，要件定義における記述，これら複数のモデル変換，および状態機械への時間制約記述からなり，計算機システムの開発段階において時間に関する扱いが異なることを示す．具体的な組み込み開発事例に対して本手法を適用し，評価した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Software reliability has became a major engineering concern, because of the prevalence of computer systems over the infrastructure of human society and the acceleration of its importance in such systems. Formal methods are studied for a variety of modeling techniques based on inherent mathematical logics. They have a long history as ways of improving software reliability. Verification of most systems is, however, not limited to a single issue but multiple properties, therefore researches about combination of several logics are the key to practical applications of formal methods. In this paper, we propose a developing procedure converting from constraints on abstract functions in requirements into explicit formal specifications mainly related to the timing property, and verification method at the design phase for the behavior of multi layered state machines in a combined way. This method is applied to a concrete embedded system as an evaluation.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2010-SE-170, 号 17, p. 1-8, 発行日 2010-11-04
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会