| 研究課題/領域番号 |
19K11914
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 仙台高等専門学校 |
|---|
研究代表者 |
岡本 圭史 仙台高等専門学校, 総合工学科, 教授 (00308214)
|
|---|
| 研究分担者 |
高井 利憲 奈良先端科学技術大学院大学, 先端科学技術研究科, 客員准教授 (10425738)
木藤 浩之 電気通信大学, 大学院情報理工学研究科, 客員研究員 (90705287)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2021年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2020年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2019年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
|
|---|
| キーワード | 数理議論学 / 数理論理学 / SMTソルバ / 仕様 / 品質向上 / 自然言語処理 / 不整合解消 / 仕様検証 |
|---|
| 研究開始時の研究の概要 |
現在のシステムは複雑であり，かつ高い信頼性・安全性が求められており，システムに組込まれるソフトウェアも複雑化している．高品質な仕様書の作成は重要な課題であるが，仕様書の品質改善は大変コストのかかる作業である．
本研究では，数理議論学に基づく仕様書の不整合解消支援法を提案し，提案手法に基づくツールを試作・評価を目的とする．数理議論学を用いることで，矛盾を含む多様な不整合の解消を支援し，大規模な仕様書の不整合解消を支援し，さらにどの記述を採用すべきかといった不整合解消の判断材料提示を支援できる．
本研究により，高品質な仕様書が得られ，結果として，開発コスト低減，製品の品質向上が期待できる．
|
| 研究成果の概要 |
本研究では，数理議論学の議論フレームワークや外延を用いることで、論理的矛盾を含めた広義の不整合に対応した不整合解消支援ツールを試作した。具体的には、機械学習ベース言語モデルを用いて、自然言語で記述された仕様書から議論フレームワークを構築する方法、特に攻撃関係（仕様書構成要素間の不整合を表す関係）を抽出する方法を提案し、実装した。また、議論フレームワーク中の外延（仕様書中の整合的な記述の集合）を一階述語論理の拡張を用いて定義することで、SMTソルバを用いて議論フレームワークから外延を列挙する方法を提案し、実装した。これらの成果を基に不整合解消支援手法を提案し、ツールとして試作した。
|
| 研究成果の学術的意義や社会的意義 |
システムはソフトウェア集約的であり、システムの信頼性は仕様書に依存する。したがって、仕様書の(整合性を含めた)品質向上は重要な課題である。しかし、仕様書の規模は大きく、不整合を検知・解消することは困難である。本研究で試作した不整合解消支援ツールを用いることで、仕様書中の不整合を自動的に検知できる。さらに本ツールが提示する外延（信頼すべき記述の候補）は、仕様記述者が不整合を解消する際のヒントとなる。他方、本研究では、自然言語処理手法を用いて不整合を検出するため、論理的矛盾を含めた広義不整合を検出できる。以上から、仕様書の品質向上に加え、仕様書の不整合解消にかかるコストの低減が期待できる。
|
