自然語解析と反例解析を活用したソフトウェア開発

使用自然语言分析和反例分析进行软件开发

基本信息

批准号：
21K11826
负责人：
岡野浩三
金额：
$ 2.5万
依托单位：
Shinshu University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2021
资助国家：
日本
起止时间：
2021-04-01 至 2025-03-31
项目状态：
未结题

项目摘要

本研究では次の学術的問題を対象とする．(RQ1) 自然語による仕様記述から状態遷移モデルや検証性質等，形式的仕様記述へ適切に変換する方法論はあるのか?(RQ2) モデル検査の反例の有効活用はどこまでできるか? (RQ3) STAMP/STPA と自然言語処理，形式手法との連携方法は? 今年度は機械学習をもちいたソフトウェア開発、自然言語処理を用いた要求仕様解析、時間オートマトンのモデル検査ツールの開発の３点で大きく進展した。機械学習をもちいたソフトウェア開発ではJavaを対象にモデル検査の出力の可読性向上のを図る方法について成果をだした。また、ソフトウェアのバグ限定手法であるフォールトローカライゼーションを従来の通り、統計的指標を用いる方法ではなく、機械学習を応用する方法を改良することによって、より精度良く行う方法を考案し、研究会や国際会議で発表をおこなった。要求仕様書の自然語解析を形態素解析と構文解析を組みわせて行い、状態遷移図作成に必要な要素を抽出する研究を精力的に行い、特にラムダカリキュラスを用いた時間関係推論を活用した方法論を考案し、複数の情報システムに活用し、国際会議で発表を行った。この研究成果をさらに発展させ、機械学習を活用した要求仕様の解析に取り組み始めている。時間オートマトンを用いたモデル検査についてはSMT/SAT式に帰着する方法論をさらに一般時間オートマトンに拡張する方法を実装し、ツールとして実装することに成功した。この結果を国際会議に発表した。

这项研究涵盖了以下学术问题：（RQ1）是否有一种方法可以将自然语言中的规范适当地转换为正式规范说明，例如国家过渡模型和验证属性？（RQ2）我们可以有效利用模型检查的反例？（RQ3）邮票/STPA如何与自然语言处理和形式方法合作？今年，我们以三种方式取得了长足的进步：使用机器学习的软件开发，使用自然语言处理对所需规范进行分析以及为时间自动机的模型检查工具的开发。在使用机器学习的软件开发中，我们产生了有关如何提高Java模型检查输出的可读性的结果。此外，与以前一样，我们设计了一种实现故障本地化的方法，一种用于软件的错误限制方法，通过改进应用机器学习而不是使用统计指标的方法，并在研究会议和国际会议上提出。他通过结合词素分析和句法分析对所需规范进行了自然语言分析，并积极进行了研究以提取创建状态过渡图所需的要素，并设计了一种使用Lambda Curriculus的时间相关推理的方法，并在多个信息系统中使用了IT，并在国际会议上呈现了。研究结果已得到进一步开发，并开始使用机器学习来分析所需的规格。对于使用Time Automata进行模型检查，我们已经实施了一种方法来进一步扩展导致SMT/SAT表达式的方法，并将其成功实现为工具。结果是在国际会议上提出的。