研究課題/領域番号 |
19K11914
|
研究種目 |
基盤研究(C)
|
配分区分 | 基金 |
応募区分 | 一般 |
審査区分 |
小区分60050:ソフトウェア関連
|
研究機関 | 仙台高等専門学校 |
研究代表者 |
岡本 圭史 仙台高等専門学校, 総合工学科, 教授 (00308214)
|
研究分担者 |
高井 利憲 奈良先端科学技術大学院大学, 先端科学技術研究科, 客員准教授 (10425738)
木藤 浩之 電気通信大学, 大学院情報理工学研究科, 客員研究員 (90705287)
|
研究期間 (年度) |
2019-04-01 – 2022-03-31
|
キーワード | 数理議論学 / 数理論理学 / SMTソルバ / 仕様 / 品質向上 / 自然言語処理 |
研究成果の概要 |
本研究では,数理議論学の議論フレームワークや外延を用いることで、論理的矛盾を含めた広義の不整合に対応した不整合解消支援ツールを試作した。具体的には、機械学習ベース言語モデルを用いて、自然言語で記述された仕様書から議論フレームワークを構築する方法、特に攻撃関係(仕様書構成要素間の不整合を表す関係)を抽出する方法を提案し、実装した。また、議論フレームワーク中の外延(仕様書中の整合的な記述の集合)を一階述語論理の拡張を用いて定義することで、SMTソルバを用いて議論フレームワークから外延を列挙する方法を提案し、実装した。これらの成果を基に不整合解消支援手法を提案し、ツールとして試作した。
|
自由記述の分野 |
数理論理学、形式手法、安全分析
|
研究成果の学術的意義や社会的意義 |
システムはソフトウェア集約的であり、システムの信頼性は仕様書に依存する。したがって、仕様書の(整合性を含めた)品質向上は重要な課題である。しかし、仕様書の規模は大きく、不整合を検知・解消することは困難である。本研究で試作した不整合解消支援ツールを用いることで、仕様書中の不整合を自動的に検知できる。さらに本ツールが提示する外延(信頼すべき記述の候補)は、仕様記述者が不整合を解消する際のヒントとなる。他方、本研究では、自然言語処理手法を用いて不整合を検出するため、論理的矛盾を含めた広義不整合を検出できる。以上から、仕様書の品質向上に加え、仕様書の不整合解消にかかるコストの低減が期待できる。
|