Vol.3 No.1 2010

69/110

Research paper : A field-scientific approach to Clinico-Informatics (Y. Kinoshita et al.)−66−Synthesiology - English edition Vol.3 No.1 (2010) theories in temporal logic is our principal concern here. A model of a formal theory in temporal logic is usually given in the form of a transition systemNote 4).Software which automatically performs model checking is called a model checker. A model checker is given two input data: a model and a property expected to hold for the model. The model checker reponds on whether the former satisfies the latter in the form of YES or NO. When the answer is NO, it normally gives a counterexample, too. In the case that the formal theory is in temporal logic, a model checker usually gives a counterexample in the form of an execution trace (state sequence) of the transition system. Hereafter, we only consider model checkers for formal theories in temporal logic; so the formal theory concerning model checkers is assumed to be in temporal logic.Faults in an information system may be detected using a model in the following way. First, a user defines a transition system that represents the system. The transition system will work as a model of the formal theory of concern. Now, information systems are in the real world, while transition systems are in the mathematical world. So, the defined transition system is different from the information system. We say that the transition system is obtained from the information system through (mathematical) abstraction. While abstracting the information system, one intends to retain every feature which affects the addressed property. There are, however, no mathematical ways to make sure that every such feature is really retained, since the information system lies outside the mathematical world. The defined transition system may not sufficiently retain the property of the original information system. We shall come back to this problem later. Hereafter in this chapter, we shall exclusively consider the transition system rather than the original information system to be verified, unless otherwise stated.Now, whether the transition system has the expected property boils down to whether the property is true under the model given as a transition system. So, it can be checked by a model checker. If the model checker answers NO and gives a counterexample, which indicates a candidate of the malfunction of the original information system, then the counterexample, given in terms of execution trace of transition system, is interpreted in terms of the original information system and judgment whether it does give an example of malfunction of the original system is done by the information system designer, not the verification engineer. Even if the model checker says YES (satisfied), however, it does not necessarily mean that there are no faults in the original information system (false positive). This is because it is not clear whether the transition system given as a model adequately represents the original information system.As shown above, the model checker checks the transition system. To use the model checker to check the original information system, some manipulation is necessary to fill in the gap between the original information system and the transition system. For example, even if the model checker answers NO, one cannot conclude immediately that there is a fault in the system (false negative), and the counterexample should be analyzed. The issue is who does such analysis. Ideally, someone from the development team participates in the analysis in addition to the people doing the verification (fault finding), and the final decision on whether it is a fault or not is done by the development team.3 Field scientific method of technology transferIn this chapter, we give a systematic account of technology transfer by applying the W-model for problem solving attributed to Kawakita. The Full Research model, which has been discussed since the establishment of AIST, is also applied and is compared with Kawakita’s model.3.1 Kawakita’s W-model for problem-solvingKawakita observed that study in science is classified into three categories: bibliographical science, experimental science, and field science[1]. Study in bibliographical science is conducted on desktop using the earlier literature by means of deduction. Mathematics is its typical example. Experimental science is an inductive study where a reproducible phenomenon is recreated in the laboratory through experiments and one investigates whether a hypothesized theory holds with respect to the phenomenon; an example is experimental physics. These two kinds of study are based on some given theory, but field science focuses upon abduction where one goes out to the field to observe a possibly non-reproducible phenomenon on site in order to set up a theory or a hypothesis. What occurs in civil society immediately after an earthquake is an excellent example of such an observation. The difference between these three kinds of study is purely methodological, and so the field is Knowledge baseObservationin the fieldExperiencelevelThinkinglevelExplorationVerificationPreparation of experimentAbduction and synthesisRaisinga questionDeduction(inference)Analysis ofthe situationHGEDCBAFObservationof experimentFig. 1 Kawakita’s W-model for problem solving. (taken from [1] and reconstructed)

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