@article{oai:ipsj.ixsq.nii.ac.jp:00203162,
 author = {來間, 啓伸 and 佐藤, 直人 and 中川, 雄一郎 and 小川, 秀人 and Hironobu, Kuruma and Naoto, Sato and Yuichiroh, Nakagawa and Hideto, Ogawa},
 issue = {2},
 journal = {情報処理学会論文誌},
 month = {Feb},
 note = {計算機システムが実世界と密に連携して動作するためには，論理的に記述・分析できない不確実性に適合するソフトウェアが必要であり，未知の入力値に対して学習データからの推論により出力値を返す機械学習の適用が注目されている．一方，このようなソフトウェアは入力データ空間が定義できず出力値に予測不能性があるため，ソフトウェアの振舞いを確率的にしか把握できない．本稿では，機械学習適用ソフトウェアの高信頼化を目的に，段階的詳細化による演繹的な開発法と機械学習による帰納的な開発法の結合についてテスト・検証の観点から述べ，開発プロセスと制約充足性テスト方法を提案する．我々のアプローチは，演繹的モジュールと帰納的モジュールを分離し，それらをつなぐ部分仕様を設定するとともに，前者については部分仕様が満たされることを前提に論理的な検証を行う一方，後者についてはテストにより部分仕様の充足確率を評価し，論理的な検証結果に確率を付与する．これにより，帰納的に開発した機械学習適用モジュールと演繹的に開発した論理モジュールを，システムの信頼性評価のもとで整合的に結合する．形式手法Event-Bを用いたケーススタディにより，実現可能性を評価した．, 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.},
 pages = {407--416},
 title = {演繹的開発手法と帰納的開発手法の結合に基づく機械学習適用ソフトウェアの形式検証とテスト},
 volume = {61},
 year = {2020}
}