| 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
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2021: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2020: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2019: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | 数理議論学 / 数理論理学 / SMTソルバ / 仕様 / 品質向上 / 自然言語処理 / 不整合解消 / 仕様検証 |
|---|
| Outline of Research at the Start |
現在のシステムは複雑であり，かつ高い信頼性・安全性が求められており，システムに組込まれるソフトウェアも複雑化している．高品質な仕様書の作成は重要な課題であるが，仕様書の品質改善は大変コストのかかる作業である．
本研究では，数理議論学に基づく仕様書の不整合解消支援法を提案し，提案手法に基づくツールを試作・評価を目的とする．数理議論学を用いることで，矛盾を含む多様な不整合の解消を支援し，大規模な仕様書の不整合解消を支援し，さらにどの記述を採用すべきかといった不整合解消の判断材料提示を支援できる．
本研究により，高品質な仕様書が得られ，結果として，開発コスト低減，製品の品質向上が期待できる．
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
システムはソフトウェア集約的であり、システムの信頼性は仕様書に依存する。したがって、仕様書の(整合性を含めた)品質向上は重要な課題である。しかし、仕様書の規模は大きく、不整合を検知・解消することは困難である。本研究で試作した不整合解消支援ツールを用いることで、仕様書中の不整合を自動的に検知できる。さらに本ツールが提示する外延（信頼すべき記述の候補）は、仕様記述者が不整合を解消する際のヒントとなる。他方、本研究では、自然言語処理手法を用いて不整合を検出するため、論理的矛盾を含めた広義不整合を検出できる。以上から、仕様書の品質向上に加え、仕様書の不整合解消にかかるコストの低減が期待できる。
|
