Quantitative extension of formal models and its application to software analysis
| Project/Area Number |
19H04083
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
Seki Hiroyuki 名古屋大学, 情報学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥17,160,000 (Direct Cost: ¥13,200,000、Indirect Cost: ¥3,960,000)
Fiscal Year 2021: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2020: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2019: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
|
|---|
| Keywords | ソフトウェア検証 / モデル検査 / プログラム自動合成 / レジスタオートマトン / 形式言語理論 / 量的情報流 / 線形時相論理 / セキュリティ / ゲーム構造 / アクティブ学習 / 重み付き文脈自由文法 / mu-計算 / プログラム合成 / XML |
|---|
| Outline of Research at the Start |
ソフトウェアの信頼性を担保するための数理的解析・検証技術を実用システムに適用可能にするためには，対象とする系をデータ値，時間，確率，情報量等の量的概念を考慮した数理的モデルに拡張する必要がある．本研究ではこのような問題意識のもとに，量的情報流の動的解析，データ値をもつ計算モデルとその構造化文書処理への応用，および，重みをもつ計算モデルとそのソフトウェアコスト解析への応用の３つの課題に取り組む．それぞれの課題において，オートマトンや形式文法に基づく適切な計算モデルを設定し，基本問題の計算量の解析，効率のよいアルゴリズムの開発，および，ツールの試作と実験に基づく提案手法の有効性の評価を行う．
|
| Outline of Final Research Achievements |
We studied on the following three research topics. First, we proposed two notions on dynamic quantitative information flow (QIF), analyzed the complexity for computing these QIFs and implemented a tool for computing these QIFs based on model counting tools. Second, we investigated the complexity of basic problems on register context-free grammar (RCFG). We then proposed generalized RCFG and provided a sufficient condition for an RCFG to have decidability property on basic problems. As an application of register models to software verification, we studied LTL (linear-time temporal logic) model checking for register pushdown systems. We also proposed a subclass of mu-calculus with the freeze quantifiers which are equivalent to register automata. Furthermore, we investigated the reactive synthesis from visibly register pushdown automata. Third, we introduced the optimal run problem for weighted register automata and analyzed its complexity.
|
| Academic Significance and Societal Importance of the Research Achievements |
ソフトウェアの信頼性を保証する方法論を確立することは現代社会の喫緊の課題である．本研究の成果は，長年にわたり蓄積されたソフトウェア検証の理論的成果をさらに現実の問題に応用可能とするため，情報漏洩量，データ値および重みといった量的概念を組み込んだ数理モデルに対して，ソフトウェアの信頼性を保証する手法を与えたことに学術的および社会的意義がある．例えば，有限状態モデルにデータ値を扱う能力を加えると容易に基本問題が判定不能となってしまうが，本手法におけるレジスタモデルではデータ値の操作に合理的制約を加えることにより，重要な基本問題の判定可能性を失うことなく拡張が可能となっている．
|
Report
(4 results)
Research Products
(24 results)
