Vol.3 No.3 2010

Research paper : A methodology for improving reliability of complex systems (A. Katoh et al.)−201−Synthesiology - English edition Vol.3 No.3 (2010) when the counterexamples are analyzed, it means that the specification of the target based on the models has flaws.The following two effects can be expected by applying model checking. First, it may be possible to reduce the cost of detecting flaws in the specification by using the counterexamples. If results of test method and simulation method come out incorrect, it is necessary to analyze the cause by hypothesizing the many causes which may lead to incorrectness. Much effort may be necessary to identify the real cause. By applying model checking, it is possible to trace the occurrence of incorrectness using the counterexamples which are output from the model checking tool automatically. Therefore, it is possible to identify the cause of incorrectness efficiently. Second, there is a possibility for detecting flaws in the specification to be verified through modeling, or the formalization of specification, when model checking is conducted.4 Synthesis of methods Architectural design method and model checking are synthesized while taking advantage of the characteristics of each method, to construct the methodology for this research. In this chapter, the process of synthesizing architectural design method and model checking is shown by describing workflows in this methodology.4.1 Proposed methodology Figure 6 shows the methodology proposed for this research, whereby architectural design method and model checking are synthesized. This methodology is composed of architectural design method, model checking, and bridge methodTerm23 which connects two methods.First, a system specification is input to this methodology. Based on the system specification, architectural designing including functional and physical designing are done according to IEEE 1220. By architectural designing, the system specification is decomposed into component specifications and interface specifications among the components (dashed-line specifications in upper left in Fig. 6). A traceability matrixTerm 24 defined in IEEE 1220 is developed in the process of architectural designing. Figure 7 shows the traceability matrix. An identification number is assigned to each specification for the system specification and the component specifications. The traceability matrix summarizes the correspondence between the system specification and component specifications which are broken down from the system specification.Next, bridge method developed in this research is applied to the component specifications, the interface specifications among components, the traceability matrix, and the system specification. By applying the bridge method, specifications related to the cooperative behavior are extracted from the component specifications and interface specifications among components (striped specifications in lower left of Fig. 6). Properties which must be satisfied by the cooperative behavior are derived. A model checking tool which is applied in the methodology is selected. Outputs of the bridge method are necessary inputs for conducting model checking.Specifications related to the cooperative behavior extracted from the component specifications and interface specifications Fig. 6 Methodology in this researchFig. 7 Traceability matrixInputMethodologyInconsistencyof cooperativebehaviorTraceabilitymatrixComponentBspecificationBridge methodInterfacespecificationbetweencomponentsComponentAspecificationArchitecturaldesigningSystemspecificationComponent AspecificationforcooperativebehaviorComponent BspecificationforcooperativebehaviorInterfacespecificationbetweencomponents forcooperative behaviorProperties tobe satisfiedEvery property is not satisfiedEvery property is satisfiedConsistency is confirmed for cooperative behaviorComponentAspecificationComponentBspecificationInterfacespecificationbetweencomponentsWorkflowOutputModel checkingModelchecking toolRelease5.3 function ZB5.2 function YB5.1 function XB5.1 function XA5.2 function YA15.3 function YA24.3 function Z4.2 function Y4.1 function X4.3 function Z4.2 function Y4.1 function XTraceability matrix for systemspecification andcomponent B specificationTraceability matrix for systemspecification andcomponent A specification5.1 function XB5.2 function YB5.3 function ZB4.1 function X4.2 function Y4.3 function ZSystem specificationN/A5.3 function YA25.2 function YA15.1 function XAComponent A specificationSystem specificationComponentBspecificationComponentAspecificationSystemspecification6Component B specification


page 16