Vol.3 No.3 2010

Research paper : A methodology for improving reliability of complex systems (A. Katoh et al.)−212−Synthesiology - English edition Vol.3 No.3 (2010) advantages. Please describe what other tools there were and what their disadvantages were. Similarly, if there were other candidates in the selection of UPPAAL, please describe them.Answer (Atsushi Katoh)In this research, we employed the research policy of selecting the methods for which the effectiveness has been already established, to efficiently establish a high-quality methodology. In constructing this methodology, we applied architectural design method that has been recognized as being effective and is standardized. Other system design methods include structured analysis and structured design (SA/SD) method. While architectural deign method is not appropriate for system design focusing on specific technological elements such as data or service, it is a universal design method independent of any particular technological systems. Therefore, we selected architectural design method as our system design method. The representative system engineering standards for architectural design method include ISO 15288, ANSI/EIA 632, and IEEE 1220. Since the tasks and procedures are finely defined for each process in IEEE 1220, we employed IEEE 1220. These standards are compared in chapter 3.Model checking is a method that has already been established as a verification method. The research was started in the early 1980s, and today, it is widely used in software development. Model checking is “a verification using models”, but it has become a proper noun for the verification method. We will add these points to chapter 1. The system verification methods other than model checking include test method and simulation method. However, model checking can exhaustively verify whether the properties to be satisfied for the state transitions are valid or not. Therefore, we employed model checking as our system verification method. We will compare these in chapter 3.There is a verification method called theorem proving in the formal method. Theorem proving is a method where the system specifications and designs are described in a language that is mathematically defined in terms of semantics, and are given exact proof. While theorem proving enables exact verification of a system, great efforts are needed because some parts must be done interactively with humans. The authors think that theorem proving is not a verification method that has been applied in industry and the effectiveness has not been demonstrated. Therefore, we excluded it from the candidates of verification methods of this research.The representative types of model checking include finite automaton and timed automaton, which is an extended finite automaton. Model checking and the tools to be applied must be selected according to the characteristic of the verified target. In a case of verifying general state transitions where the situation change is triggered by some external event, we select a model checking tool corresponding to finite automaton. SPIN is a representative model checking tool. In a case of verifying state transitions including temporal limitations, we select a model checking tool that corresponds to timed automaton. UPPAAL is another representative model checking tool. If the target that can be verified by model checking for finite automaton, it can also be verified using a model checking tool for timed automaton. However, it does not work the other way around. We will add these points to chapter 4. In the applied case, it was necessary to verify the temporal limitations of the cooperative behavior. Also, for the model checking tool corresponding to timed automaton, the authors determined that only UPPAAL possesses the applicable quality in the industrial case.4 Industrial application of the outcomesComment (Kanji Ueda)I think the significance as Type 2 Basic Research will increase if you address how the result of this research was actually used in the industrial application, what is the prospect, and the limit of application if it is used.Comment (Motoyuki Akamatsu)The important point of this research is that this methodology must be used by the people in industry who actually work to develop the system. In that sense, I would like to see an explanation on what targets these outcomes can be used, and the range of its application. Also, please state your thoughts on the ways of diffusing this methodology.Answer (Atsushi Katoh)I think the methodology in this research can be applied to the development of any technological systems, without specializing in particular technological systems. The reason is that when a system is designed, the function is achieved by finding the components that compose the system based on the system specifications, and then have the components behave cooperatively, and this is a common concept for all technological systems. Also, this methodology can deal with the unique issues of cooperative behavior in the applied system. The reason is that this methodology has the bridge method where the attributes and the model checking tool are selected according to the characteristics of the cooperative behavior.Currently, the authors are planning and developing a new product for the industrial robot jointly with an industrial robot company. The industrial case study in chapter 5 describes these efforts. As of writing of this paper, the industrial robot is being developed according to the specifications that were verified for consistent cooperative behavior by applying the methodology of this research. I think this research amounts to Type 2 Basic Research because of the contribution to increase the reliability of industrial robot. These points are added to chapter 5.However, cautions must be taken when applying this methodology. This method employs model checking to verifiy consistency of the cooperative behavior by components. When there are numerous states in model checking, state explosion may occur where model checking cannot be completed due to the huge number of combinations of the states. This means that if the cooperative behavior by components becomes extremely complex due to architectural designing, the verification of the cooperative behavior may not get completed in model checking. In such cases, it is necessary to do re-architectural designing to ensure the cooperative behavior by components will not become extremely complex, or the number of the states in the models for the specifications related to the cooperative behavior must be reduced. We will describe these in the newly added section “Applicability of this methodology” in chapter 6.This methodology will be spread throughout industry by Keio SDM to which the authors belong. We will add this to chapter 7.5 Advantages and disadvantages of the selected methodsQuestion (Motoyuki Akamatsu)In chapter 3, you describe the selection of the methods. You mention architectural design and SA/SD methods for achieving function “a”, and state that you selected architectural design method because it is a universal design method, although it is not suitable for system design focusing on specific technological elements such as data or service. Since the elemental technologies are selected according to the research goal, can you clearly state the goal, and then explain that you selected architectural design method as a result of comparing the advantages and disadvantages?The goal of this research, I assume, is to construct a universal methodology, but when universality is set as a goal, you will also have a problem that the methodology cannot be applied to


page 27