2021 Fiscal Year Final Research Report
Developing a tool to assist in resolving specification inconsistencies based on mathematical argumentation theory
| Project/Area Number |
19K11914
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Sendai National College of Technology |
|---|
Principal Investigator |
Okamoto Keishi 仙台高等専門学校, 総合工学科, 教授 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
高井 利憲 奈良先端科学技術大学院大学, 先端科学技術研究科, 客員准教授 (10425738)
木藤 浩之 電気通信大学, 大学院情報理工学研究科, 客員研究員 (90705287)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 数理議論学 / 数理論理学 / SMTソルバ / 仕様 / 品質向上 / 自然言語処理 |
|---|
| Outline of Final Research Achievements |
In this research project, by using argumentation frameworks and extensions of mathematical argumentation theory, we have developed a prototype inconsistency resolution support tool for inconsistencies in a broad sense, including logical contradictions. In particular, we proposed and implemented a method for constructing an argumentation framework from a specification document written in natural language using a machine learning-based language model. Moreover, we have proposed a method for extracting attack relations (relations representing inconsistencies among specification elements). We also proposed and implemented a method for enumerating extensions from the argumentation framework using SMT solvers by defining extensions (sets of consistent descriptions in the specification) in the argumentation framework in an extension of first-order predicate logic. Based on these results, we proposed an inconsistency resolution support method and prototyped it as a tool.
|
| Free Research Field |
数理論理学、形式手法、安全分析
|
| Academic Significance and Societal Importance of the Research Achievements |
システムはソフトウェア集約的であり、システムの信頼性は仕様書に依存する。したがって、仕様書の(整合性を含めた)品質向上は重要な課題である。しかし、仕様書の規模は大きく、不整合を検知・解消することは困難である。本研究で試作した不整合解消支援ツールを用いることで、仕様書中の不整合を自動的に検知できる。さらに本ツールが提示する外延（信頼すべき記述の候補）は、仕様記述者が不整合を解消する際のヒントとなる。他方、本研究では、自然言語処理手法を用いて不整合を検出するため、論理的矛盾を含めた広義不整合を検出できる。以上から、仕様書の品質向上に加え、仕様書の不整合解消にかかるコストの低減が期待できる。
|
