| Item type |
Journal(1) |
| 公開日 |
2020-02-15 |
| タイトル |
|
|
タイトル |
演繹的開発手法と帰納的開発手法の結合に基づく機械学習適用ソフトウェアの形式検証とテスト |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Formal Verification and Testing of Machine Learning Based Software Using Combination of Deductive and Inductive Development Methods |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[特集：組込みシステム工学] 機械学習工学，ソフトウェア品質評価，ソフトウェア開発プロセス，ニューラルネットワークの頑健性 |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
株式会社日立製作所研究開発グループ |
| 著者所属 |
|
|
|
株式会社日立製作所研究開発グループ |
| 著者所属 |
|
|
|
株式会社日立製作所研究開発グループ |
| 著者所属 |
|
|
|
株式会社日立製作所研究開発グループ |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd., Research & Development Group, Yokohama Research Laboratory |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd., Research & Development Group, Yokohama Research Laboratory |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd., Research & Development Group, Yokohama Research Laboratory |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd., Research & Development Group, Yokohama Research Laboratory |
| 著者名 |
來間, 啓伸
佐藤, 直人
中川, 雄一郎
小川, 秀人
|
| 著者名(英) |
Hironobu, Kuruma
Naoto, Sato
Yuichiroh, Nakagawa
Hideto, Ogawa
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
計算機システムが実世界と密に連携して動作するためには，論理的に記述・分析できない不確実性に適合するソフトウェアが必要であり，未知の入力値に対して学習データからの推論により出力値を返す機械学習の適用が注目されている．一方，このようなソフトウェアは入力データ空間が定義できず出力値に予測不能性があるため，ソフトウェアの振舞いを確率的にしか把握できない．本稿では，機械学習適用ソフトウェアの高信頼化を目的に，段階的詳細化による演繹的な開発法と機械学習による帰納的な開発法の結合についてテスト・検証の観点から述べ，開発プロセスと制約充足性テスト方法を提案する．我々のアプローチは，演繹的モジュールと帰納的モジュールを分離し，それらをつなぐ部分仕様を設定するとともに，前者については部分仕様が満たされることを前提に論理的な検証を行う一方，後者についてはテストにより部分仕様の充足確率を評価し，論理的な検証結果に確率を付与する．これにより，帰納的に開発した機械学習適用モジュールと演繹的に開発した論理モジュールを，システムの信頼性評価のもとで整合的に結合する．形式手法Event-Bを用いたケーススタディにより，実現可能性を評価した． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
As computer systems are closely related to the real world, software is required to adopt the uncertain phenomena that cannot be described nor analyzed logically. Machine learning is expected to be a promising way to develop software that accommodate such uncertainty, since it makes outputs induced from the given learning data set even for unknown inputs. The input data space of machine learning based software cannot be defined and it is substantially impossible to predict its outputs. The behavior of such software can be analyzed only in a statistical way. In this paper, we describe a reliable software development method in which the machine learning based inductive development is combined with the refinement based deductive development at a point of testing and formal verification and propose a development process and conformance testing. Out approach is composed of: 1. separating deductive module and inductive module and placing a partial specification connecting them, 2. verifying the deductive module with the assumption that the partial specification is fulfilled, 3. evaluating the probability the inductive module fulfills the partial specification by conformance testing, 4. assigning the probability to the verified properties of the deductive module. We show a case study using Event-B formal method and discuss the feasibility of our approach. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AN00116647 |
| 書誌情報 |
情報処理学会論文誌
巻 61,
号 2,
p. 407-416,
発行日 2020-02-15
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7764 |
IPSJ-JNL6102034.pdf (609.5 kB)
