As one type of machine-learning model, a “decision-tree ensemble model” (DTEM) is represented by a set of decision trees. A DTEM is mainly known to be valid for structured data; however, like other machine-learning models, it is difficult to train so that it returns the correct output value (called “prediction value”) for any input value (called “attribute value”). Accordingly, when a DTEM is used in regard to a system that requires reliability, it is important to comprehensively detect attribute values that lead to malfunctions of a system (failures) during development and take appropriate countermeasures. One conceivable solution is to install an input filter that controls the input to the DTEM and to use separate software to process attribute values that may lead to failures. To develop the input filter, it is necessary to specify the filtering condition for the attribute value that leads to the malfunction of the system. In consideration of that necessity, we propose a method for formally verifying a DTEM and, according to the result of the verification, if an attribute value leading to a failure is found, extracting the range in which such an attribute value exists. The proposed method can comprehensively extract the range in which the attribute value leading to the failure exists; therefore, by creating an input filter based on that range, it is possible to prevent the failure. To demonstrate the feasibility of the proposed method, we performed a case study using a dataset of house prices. Through the case study, we also evaluated its scalability and it is shown that the number and depth of decision trees are important factors that determines the applicability of the proposed method.

A practical model-checking (MC) approach for fault analysis, that is one of the most cost-effective tasks in software development, is proposed. The proposed approach is based on a technique, named “Program-oriented Modeling” (POM) for extracting a model from source code. The framework of model extraction by POM provides configurable abstraction based on user-defined transformation rules, and it supports trial-and-error model extraction. An environment for MC called POM/MC was also built. POM/MC analyzes C source code to extract Promela models used for the SPIN model checker. It was applied to an industrial software system to evaluate the efficiency of the configurable model extraction by POM for fault analysis. Moreover, it was shown that the proposed MC approach can reduce the effort involved in analyzing software faults by MC.