| 研究課題/領域番号 |
19H04083
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
|
|---|
| 研究分担者 |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | ソフトウェア検証 / モデル検査 / プログラム自動合成 / レジスタオートマトン / 形式言語理論 / 量的情報流 / 線形時相論理 / セキュリティ |
|---|
| 研究成果の概要 |
ソフトウェアの信頼性を保証する手法として，量的情報流の動的解析，データ値を扱う計算モデル，重み付き計算モデルの３つの課題について研究を行った．動的情報流の２つの定義を提案し，その計算量解析を行うとともに，モデル計数ツールを用いた実装を行った．レジスタ計算モデルについて，レジスタ付きCFGの基本問題の計算量を明らかにするとともに，比較演算子に着目したRCFGの一般化，RCFGに対応するレジスタ付きPDSのLTLモデル検査アルゴリズム，レジスタオートマトンと能力等価な凍結演算子付きmu-計算の部分クラスを提案した．重み付きレジスタオートマトンの最小重み実行問題の計算量を明らかにした．
|
| 自由記述の分野 |
ソフトウェア基礎理論
|
| 研究成果の学術的意義や社会的意義 |
ソフトウェアの信頼性を保証する方法論を確立することは現代社会の喫緊の課題である．本研究の成果は，長年にわたり蓄積されたソフトウェア検証の理論的成果をさらに現実の問題に応用可能とするため，情報漏洩量，データ値および重みといった量的概念を組み込んだ数理モデルに対して，ソフトウェアの信頼性を保証する手法を与えたことに学術的および社会的意義がある．例えば，有限状態モデルにデータ値を扱う能力を加えると容易に基本問題が判定不能となってしまうが，本手法におけるレジスタモデルではデータ値の操作に合理的制約を加えることにより，重要な基本問題の判定可能性を失うことなく拡張が可能となっている．
|
