Vol.3 No.3 2010
Research paper : A methodology for improving reliability of complex systems (A. Katoh et al.)−205−Synthesiology - English edition Vol.3 No.3 (2010) on the properties which must be satisfied by the cooperative behavior. For the measurement and integrated control subsystems, the formulae for 23 cases are developed based on the properties which must be satisfied by the cooperative behavior according to UPPAAL expression form. Table 2 shows the formulae corresponding to the two items shown in Table 1.Model checking is conducted based on the developed models and the formulae. For the measurement and integrated control subsystems, model checking using UPPAAL is conducted based on the cooperative behavior models shown in Figs. 11 to 13 and the formulae for the 23 cases including the two cases shown in Table 2. The results of model checking are analyzed. For the measurement and integrated control subsystems, the results show that the models do not satisfy some formulae. When the counterexamples output by UPPAAL are analyzed, six cases of inconsistency of the cooperative behavior are detected including the results of the formulae shown in Table 2. Table 3 shows the results of model checking corresponding to the two cases in Table 2.Inconsistency of the cooperative behavior is fed back to architectural designing. For the measurement and integrated control subsystems, architectural designing is done again, based on the six cases of inconsistent cooperative behavior including the results of Table 3. As a result of re-architectural designing, the measurement subsystem specification, the integrated control subsystem specification, and the interface specification between the measurement and integrated control subsystems whose inconsistency of the cooperative behavior is corrected, are developed.5.3 Application resultsThe methodology in this research is applied to the system specification of the irregular-rigid-body-transport robot system. As a result, the measurement subsystem specification, the integrated control subsystem specification, the robot subsystem specification and the interface specifications among the subsystems are derived from the system specification of the irregular-rigid-body-transport robot system. It is also possible to detect inconsistency of the cooperative behavior, as shown in Table 3, from the measurement and integrated control subsystems before fixing these specifications. Later, it is possible to develop the subsystem specifications and interface specifications between subsystems whose cooperative behavior is consistent. We are able to apply this methodology to the Fig. 11 Cooperative behavior model for the measurement subsystemTable 2 Formulae of the cooperative behavior for the measurement and integrated control subsystems (2 out of 23 cases)A P_BING_SCAN.BING_SCAN_REQ_STOPimply (bing_stopreq_time <= 10)3-3A (bing_syscont_sendreq == bing_req_rod)imply (bing_syscont_req == bing_req_rod)1-5FormulaNo.Table 3 Model checking results of the cooperative behavior for the measurement and integrated control subsystems (2 out of 6 cases)The measurement processing may not stop within 100 ms from receiving the measurement stop request. Also, the measurement subsystem itself may stop by receiving the measurement stop request.3-3Depending on the messages which are sent or recieved between subsystems, or the timing of processings related to the messages, the response for rigid-body measurement request/the measurement request for placement area/the measurement stop request issued before n-th time may be returned to the rigid-body measurement request issued on the n-th time.1-5Model checking resultNo.