@techreport{oai:tsurumi-u.repo.nii.ac.jp:00001068,
 author = {田辺, 良則 and TANABE, Yoshinori},
 month = {Mar},
 note = {研究成果の概要（和文）：モデル検査技術を用いてソフトウェアが正しく動作することを検証する「ソフトウェアモデル検査」において活性性質の検証に関して研究を行った．LTL論理式から作成されるBuchiオートマトンと状態空間の同期積を探索する際に，同一の状態を何度も作成するために遷移に大きなコストがかかるという点に着目し，同一状態を再利用することで平均的な実行時間を短くする方式を考案し，Java Pathfinderの上での実装を得た．, 研究成果の概要（英文）：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., ・2018(平成30)年度 科学研究費補助金 基盤研究(C) 研究成果報告書, ・研究期間 (年度)：2016-04-01 – 2019-03-31, ・研究分野：ソフトウェア工学, ・研究成果の学術的意義や社会的意義 : ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである．, 研究課題/領域番号 : 16K00109},
 title = {ソフトウェアモデル検査における活性検証},
 year = {2019}
}