ソフトウェアモデル検査における活性検証

• 資料種別: 文書・図像類
• タイトル: ソフトウェアモデル検査における活性検証
• 著者・編者: 田辺, 良則
• 著者標目: 田辺, 良則 タナベ, ヨシノリ
• 出版年月日等: 2019-03-31
• 出版年（W3CDTF）: 2019-03-31
• 並列タイトル等: Liveness verification in software model checking
• 本文の言語コード: jpn
• 件名標目: model checking; software; liveness
• 対象利用者: 一般
• 一般注記: ・2018(平成30)年度 科学研究費補助金 基盤研究(C) 研究成果報告書; ・研究期間 (年度)：2016-04-01 – 2019-03-31; ・研究分野：ソフトウェア工学; ・研究成果の学術的意義や社会的意義 : ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである．; 研究課題/領域番号 : 16K00109
• オンライン閲覧公開範囲: 限定公開
• 関連情報（URI）: URI; https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-16K00109/
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 鶴見大学 : 鶴見大学・短期大学部機関リポジトリ

• 要約等: 研究成果の概要（和文）：モデル検査技術を用いてソフトウェアが正しく動作することを検証する「ソフトウェアモデル検査」において活性性質の検証に関して研究を行った．LTL論理式から作成されるBuchiオートマトンと状態空間の同期積を探索する際に，同一の状態を何度も作成するために遷移に大きなコストがかかると...