WEKO3
アイテム
ソフトウェアモデル検査における活性検証
https://tsurumi-u.repo.nii.ac.jp/records/1068
https://tsurumi-u.repo.nii.ac.jp/records/1068a509741f-ec3b-407b-96b6-bedeec3ac31b
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
16K00109 (284.0 kB)
|
.png)
|
| Item type | 報告書 / Research Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2022-03-17 | |||||
| タイトル | ||||||
| タイトル | ソフトウェアモデル検査における活性検証 | |||||
| 言語 | ja | |||||
| タイトル | ||||||
| タイトル | Liveness verification in software model checking | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | model checking | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | software | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | liveness | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18ws | |||||
| 資源タイプ | research report | |||||
| 研究代表者 |
田辺, 良則
× 田辺, 良則 |
|||||
| 報告年度 | ||||||
| 日付 | 2019-03-31 | |||||
| 日付タイプ | Issued | |||||
| 研究課題番号 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 研究課題/領域番号 : 16K00109 | |||||
| 言語 | ja | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 研究成果の概要（和文）：モデル検査技術を用いてソフトウェアが正しく動作することを検証する「ソフトウェアモデル検査」において活性性質の検証に関して研究を行った．LTL論理式から作成されるBuchiオートマトンと状態空間の同期積を探索する際に，同一の状態を何度も作成するために遷移に大きなコストがかかるという点に着目し，同一状態を再利用することで平均的な実行時間を短くする方式を考案し，Java Pathfinderの上での実装を得た． | |||||
| 言語 | ja | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 研究成果の概要（英文）：Software model checking is a method to verify that software works properly. When verifying a liveness property, a naive method would search the synchronous product of a Buchi automaton created from a LTL formula and a state space. This method is not very effective, because a same state can be created many times. In this research, we propose a method that reduces the average cost of transition by saving and restoring states, and implemented it on Java PathFinder. | |||||
| 言語 | en | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・2018(平成30)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 | |||||
| 言語 | ja | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・研究期間 (年度)：2016-04-01 – 2019-03-31 | |||||
| 言語 | ja | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・研究分野：ソフトウェア工学 | |||||
| 言語 | ja | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・研究成果の学術的意義や社会的意義 : ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである． | |||||
| 言語 | ja | |||||
| 関連サイト | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-16K00109/ | |||||
| 著者版フラグ | ||||||
| 出版タイプ | AM | |||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
