Vol.3 No.1 2010

68/110

Research paper : A field-scientific approach to Clinico-Informatics (Y. Kinoshita et al.)−65−Synthesiology - English edition Vol.3 No.1 (2010) extremely wide. It varies from electronic and mechanical engineering to chemical process, and more. It is therefore necessary for those who study clinico-informatics to communicate with the engineers of various fields and to exchange information for analyzing and improving the diverse and the complex. Therefore, it is often necessary, as our own experience shows, to start technology transfer by conveying background knowledge such as mathematical logic that is totally foreign to the engineers. We regard it natural to consider such a process as a cross-cultural encounter and exchange. Thus, we regard the technology transfer process as a kind of cross-cultural exchange. It would then be natural to apply methods in ethnology and scientific technique of other fields to study technology transfer. The techniques to deal with diverse and complex situations include qualitative research, ethnography, and fieldwork or field science. The techniques such as interviewing, participant observation and the KJ method[1][2][3] are used in sociology and nursing as well as ethnology. Incidentally, Kyoto University, from which a respectable tradition of fieldwork has emerged, has recently proposed field informatics. They say, however, “Solutions for problems in the field are proposed from the viewpoint of informatics and the various issues that arise in the field[4],” which shows their approach is somewhat different from ours, as we would have said “Solutions for problems in informatics (or information processing) are proposed from the viewpoint of fieldwork.”The Research Center for Verification and Semantics (CVS), AIST, conducts the study of verification using the Mathematical Methods to check whether a given information system operates as intended. The properties to be verified include: deadlock-freeness (it never stuck), liveness (appropriate service will be eventually provided), termination (execution does not fall into infinite, endless loop), correctness (correct result is calculated), etc. The verification by Mathematical Methods involves the process of representing such properties by means of logical formulae and proving that the implementation of the system meets those properties. If the system has a fault, the proof should not succeed, and in that case a counterexample is often obtained. In some cases the proof is done by a person (Semiformal Methods) and in other cases it is done by a machine (Formal Methods).CVS has conducted several joint research projects with industry. Those projects are in general called fieldwork and include the study in clinico-informatics for the technology called “model checking[5][6].” We start with the analysis of the situation by talking with the partner, consider the ways of carrying out the model checking that improve the situation most effectively, and then try to transfer the technology to the partner. Methods in fieldwork such as participant observation play central roles here. The term field science was introduced by Kawakita JiroNote 1) and it includes the KJ method (named after Kawakita Jiro). We try to give a systematic account of the technology transfer process of informatics research results, using our experiences of fieldwork as examples and Kawakita’s field scientific methods as leading principles.This paper is written as follows. In chapter 2, we explain the technology called model checking, which we transferred to our partners of joint research projects. In chapter 3, we try to give a systematic account of technology transfer using Kawakita’s notion of field science and related models for problem-solving. The general scenario of technology transfer in clinico-informatics is presented in chapters 4 and 5; the scenario for technology transfer that we have conducted is described in chapter 4, and the outline of some of the element techniques used for technology transfer is explained in chapter 5. In chapter 6, we present two of the most typical technology transfer projects that we conducted, and try to evaluate the outcome. Finally in chapter 7, the proposed model for the technology transfer process is discussed, as well as issues left for future work.2 Technology transferred: model checkingThis chapter is a short introduction to the model checkingNote 2) for readers not familiar with informatics. Model checking is the technology which was used in our joint work with industry in verification and diagnosis of the system (fault removalNote 3)).Model checking is one of the technologies in software development methodology called Formal Methods. Formal Methods is, in a sense, nothing but a scientific approach to software development, where one describes and proves propositions according to mathematical logic. In application of Formal Methods, one first sets up a formal language, in which data and the propositions about them can be written as terms and formulae. Upon that language, a formal theory is built, where axioms and rules of inference are provided. Then an interpretation is given that specifies the mathematical objects and their properties as the denotations of terms and formulae of the formal language. The fact that a proposition is true under an interpretation M is written as M , and we say is true under M. An interpretation under which all axioms of the formal theory are true is called a model. When is true under any model, we write , and we say is valid. One is usually interested in the validity of propositions, but in some cases, one is rather interested whether a proposition is true or false only under a given specific model. Checking whether a proposition is true or false under a given model is called model checking. Model checking under formal theories of a special kind, i.e., formal theories in temporal logic, are target of our interest here. Temporal logic is useful in describing dynamic properties of control programs and nowadays is one of the indispensable methods in program verification. Model checking in formal

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