状態遷移表のモデル検査における LTL 検証パターン

• Item type: SIG Technical Reports(1)
• 公開日: 2009-03-11
• タイトル: 状態遷移表のモデル検査における LTL 検証パターン
• タイトル / 言語: en
• タイトル: LTL Verification Patterns for Model Checking of State Transition Matrix
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 富士ソフト株式会社
• 著者所属: 富士ソフト株式会社
• 著者所属(英): en
• 著者所属(英): FUJISOFT INCORPORATED
• 著者所属(英): en
• 著者所属(英): FUJISOFT INCORPORATED
• 著者名: 矢野, 恭平; 小池, 隆
• 著者名(英): Kyohei, Yano; Takashi, Koike
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: ソフトウェア設計の品質向上の技術として形式手法，特にモデル検査が注目されているが，産業界への普及のためには，開発者にとって使いやすいツールの提供が必要である．そこで，筆者らは状態遷移表に基づくモデル検査の支援環境を構築した．本稿では，状態遷移表のモデル検査で使用される LTL （Linear Temporal logic） の検証パターンについて議論し，モデル検査支援環境による，パターン化された LTL 検査式の自動生成と自動検査の有用性について評価する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Formal Methods, especially Model Checking, have lately drawn attention as effective methods to improve quality of software design. Although, to be widely practiced in the industry, easy to use tools for developer is necessary. So, we developed Model Checking Support Environment based on STM(State Transition Matrix). In this paper, we discuss LTL(Linear Temporal logic) verification patterns to be used to model check the STM, and evaluate the pattern-based LTL formula auto-generation and batch test functionality of Model Checking Support Environment.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2009, 号 31(2009-SE-163), p. 303-310, 発行日 2009-03-11
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会