Vol.3 No.3 2010

Research paper : A methodology for improving reliability of complex systems (A. Katoh et al.)−208−Synthesiology - English edition Vol.3 No.3 (2010) by the verification target. Therefore, the liveness of the verification target can be extracted from the specifications of the verification target or the specifications based on the verification target. However, most of the property related to safety of the verification target is not defined in the specifications of the verification target or the specifications based on the verification target. Extracting safety of the verification target depends highly on the experience and skill of engineers who use this methodology. Particularly, extracting the safety property which must be satisfied by the cooperative behavior tends to be dependent on engineers due to the complexity of the cooperative behavior.The second issue is a problem of model checking in this methodology. In model checking, the models are developed based on the specifications related to the cooperative behavior extracted from the component specifications and interface specifications among components. The component specifications and the interface specifications are often described in natural language. Therefore, in many cases, the extracted specifications are modeled manually and errors may creep into the models. This is an issue for model checking in general.The third issue is also a problem of model checking in this methodology. In model checking, the fomulae are developed based on the properties which must be satisfied by the cooperative behavior according to the expression form of the model checking tool. The formulae of the model checking are expressed by temporal operatorTerm 37 (G: globally, F: finally) called temporal logicTerm 36, path quantifierTerm 38 (A: all, E: exists), and logic operatorTerm 39 (OR, AND, NOT). However, since specialized knowledge is needed to use temporal logic, it is difficult to develop the formulae based on the properties to be satisfied by the cooperative behavior. This is also an issue for model checking in general.7 Summary and future workIn this paper, we present the methodology where the system specification is decomposed into the component specifications and the interface specifications among components for the consistent cooperative behavior among the components which compose the system. Bridge method is developed to synthesize architectural design method and model checking, and the actual example of the bridge method is presented. The results of applying this methodology to an industrial robot are shown. From the application results, it is demonstrated that this methodology is effective for the complex system used in industry. We plan to present this methodology to the industrial fields through the Graduate School of System Design and Management, Keio University[28] (Keio SDM) to which the authors belong. The Keio SDM is a graduate school where people of various fields of both humanities and sciences study. Engineers who work in the frontline of product development on systems of aerospace, information, robot, and electronics attend Keio SDM. By presenting this methodology to the engineers attending Keio SDM, we can make contribution to industry. However, there are rooms for improvements in this methodology. In the future, we will solve issue 1 which is listed in this paper. We will aim to develop a methodology of higher quality.System: a combination of interacting elements organized to achieve one or more stated purposes.Electronic equipment system: a system equipped with multiple processors which digitally process information (e.g. cellular phone).Information system: a system for business activities where multiple computers engaging in data processing are connected with a network (e.g. business system).System of systems: a composite system which is formed by multiple systems with different purposes.Cooperative behavior: a cooperation with processings of the system component and the other system components through the interface among components.Consistency of cooperative behavior: a consistent implementation of the cooperative behavior by the components in correspondence to the system specification.Systems engineering: technological methodologies to achieve systems which satisfy the required quality within a given budget and time period. It is standardized as know-hows and rules independent of the technological fields.Architectural design method: a design method to allocate functions and performances required of a system to the system components, and to define the specifications of the components and the interface among the components.Model checking: a verification method to verify whether a given property is valid or invalid in all possible state transitions which can be achieved by the models which represent the state transitions of the system, using a computer exhaustively.Formal method: a developing and verification technology where specifications are expressed using the language of mathematical logic to guarantee the correctness of the specification.IEC 61508: an international standard which determines compliance items needed to build the functional safety in the process industry, machine manufacturing, traffic transportation, medical device, and others, using electrical, electronic, and programmable electronic systems.Term 1. Term 2.Term 3.Term 4.Term 5.Term 6.Term 7.Term 8.Term 9.Term 10.Term 11.Terminologies


page 23