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