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

• Material Type: 文書・図像類
• Title: ソフトウェアモデル検査における活性検証
• Author/Editor: 田辺, 良則
• Author Heading: 田辺, 良則 タナベ, ヨシノリ
• Publication Date: 2019-03-31
• Publication Date (W3CDTF): 2019-03-31
• Alternative Title: Liveness verification in software model checking
• Text Language Code: jpn
• Subject Heading: model checking; software; liveness
• Target Audience: 一般
• Note (General): ・2018(平成30)年度 科学研究費補助金 基盤研究(C) 研究成果報告書; ・研究期間 (年度)：2016-04-01 – 2019-03-31; ・研究分野：ソフトウェア工学; ・研究成果の学術的意義や社会的意義 : ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである．; 研究課題/領域番号 : 16K00109
• Access Restrictions: 限定公開
• Related Material (URI): URI; https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-16K00109/
• Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• Original Data Provider (Database): 鶴見大学 : 鶴見大学・短期大学部機関リポジトリ

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