Vol.3 No.1 2010

72/110

Research paper : A field-scientific approach to Clinico-Informatics (Y. Kinoshita et al.)−69−Synthesiology - English edition Vol.3 No.1 (2010) While we set up the above scenario, we followed several rationales based on our experiences in our fieldwork conducted through joint research with industry. Some of the rationales are listed here.a) Some of the industrial partners asked the research team to develop an automatic checker that checks the correctness of software in response to a press of a button. The research team did not, however, agree to do it. There are at least two reasons:(I) It is known in mathematical logic that there is no such general procedure that automatically proves whether an arbitrary given program satisfies an arbitrary given specification (undecidability of Church’s first-order predicate logic).(II) Even though the model checker itself is an automatic checker, the whole verification process using it is an interactive process because the property to be checked is usually found by try and error. On some occasions the property must be changed because there was a misunderstanding or impreciseness in setting it up; on other occasions, too much resource, memory or CPU time, is required by the verification software that the property must be divided into smaller ones or some other action is necessary. Such iteration seems to be inherently interactive and non-automatic, so, the research team was rather negative against the effort to increase the degree of automation.It seems our industrial partner wished (I) because they considered the technology transfer for detecting faults by model checking as merely a flow of information. However, it involved a more complex phenomenon than a mere flow of information, as described in b) in the actual technology transfer process.b) The verification technique, including model checking that we used as the subject of technology transfer, is a part of design technique. Design is a dynamic process rather than a static knowledge. The written texts and lectures on technical information does not convey by themselves the whole skill needed. It was necessary to convey the way how one uses the knowledge in a face-to-face manner. Here we see a kind of cross-cultural encounter; the culture of engineering or industry and the culture of academia. Incidentally, this is the reason why the technology transfer must be done as a joint work with a research team and an industrial partner, rather than as a contract and merely delegating the whole work to either side.To exemplify how the basic knowledge differs from one field to another, take the basics of mathematical logic, which is necessary to describe the logical formula to be checked in verification. Such subject is not taught at all in high schools and in most university courses, as opposed to basics of linear algebra and analysis. Even most university courses in computer science in Japan do not teach it. So there is a rather large gap between the engineer’s background and what is required for a person who uses model checking in verification in industry. According to our experience, it normally takes a few months or even a year to fill this gap, i.e., to teach the necessary basic facts about mathematical logic to the engineers who need to acquire model checking technique.c) Another reason for us to employ fieldwork for technology transfer is that we have to show to the management of our industrial partner how effective the technology of concern is in the context of actual work done at their own site.For our industrial partner to fully deploy the technology, it is necessary for them to evaluate the technology with their own eyes in their own context. But it takes time for the situation to come to that stage, as we wrote in 3 in the scenario, and the scientist in charge can often be frustrated, which of course would result in no good results. With the slogan of “moving from entrance to backyard” in mind, the scientist in the research team should try to observe where in the stage of technology transfer he/she stands, and that helps him/her keep himself/herself away from any frustration.d) Each fieldwork project started training or education of engineers individually, but it did not take long for us to realize the need of a systematic way of training. We needed an education specifically meant for engineers at work. Therefore, we developed an independent training course of model checking for engineers and have provided it to the project participants[12]. The course has been designed so that the engineers are thoroughly drilled on the basics of mathematical logic, and that the facts independent of each particular tools are emphasized and clearly distinguished from tool-dependent knowledge.e) The goal of model checking technology transfer is diverse. How our industrial partner wishes to incorporate the technology of model checking into their own development process differs much according to their culture and strategy. Some industrial partners tried to eliminate dependency on experts as much as possible by means of providing manuals. Other industrial partners tried, on the contrary, to depend on experts as much as possible, so we first trained a small number of engineers, and then those engineers trained other engineers after going back to industry.Finally, we discuss which step of our scenario corresponds to which process of Kawakita’s W-model for problem-solving. 1) The interview corresponds to the exploration on the leftmost

※このページを正しく表示するにはFlashPlayer9以上が必要です