Vol.3 No.3 2010
15/60

Research paper : A methodology for improving reliability of complex systems (A. Katoh et al.)−200−Synthesiology - English edition Vol.3 No.3 (2010) possible to decompose a complex system into its components smoothly and surely. Architectural design method in IEEE 1220 has been used in various industrial fields, and has produced results. Therefore, a certain level of effectiveness is guaranteed[16].3.2 Model checkingFigure 5 shows the process of model checking. The process of model checking can be categorized into four works: developing models, developing fomulae, conducting model checking, and analizing the model checking results. First, state transitions of a target to be verified are modeled based on the target specification according to the expression form of a model checking tool to be applied. Next, properties which must be satisfied by the verification target are considered. Formulae which express the properties are developed according to the expression form of the model checking tool. Then, the models and the formulae are input to the model checking tool on a computer, and model checking is conducted. Model checking verifies whether the models satisfy the properties expressed by formulae or not in all state transitions achievable by the models exhaustively. Finally, results of whether the models satisfy the properties expressed by formulae or not are analyzed based on outputs from the model checking tool. If the models satisfy the formulae, it means that the specification based on the models satisfy the properties. If the models do not satisfy the formulae, the state transitions of the models up to the state where the property is not valid are output as the counterexamples, If no errors are found in the models Fig. 2 Process of architectural designingFig. 4 Process of physical designing in IEEE 1220[11]DevelopingdocumentComponentBspecificationArchitecturaldesigningDevelopingactivityWorkflowinterfacespecificationbetweencomponentsComponentAspecificationSystemspecificationPhysical designingFunctional designingDefine subfunctions Define subfunctions states and modes Define functionalFailure modesAnd effects Define safetymonitoringfunctions6.3.2 Functional decomposition 6.3.2.26.3.2.36.3.2.46.3.2.56.3.2.66.3.2.1Analyze functional behaviors Define functional interface Allocate performance requirements Functional analysis 6.3.1 Functional context analysis 6.36.3.36.3.1.16.3.1.26.3.1.3Define functionaltimelinesDefine data andControl flowsEstablish functional architectureFig. 3 Process of functional designing in IEEE 1220[11]Assess technology requirementsDefine physical InterfacesIdentify off-the-shelf availabilityIdentify make or buy alternativesGroup and allocate functionsSynthesisIdentify design solution alternativesAssess safety and environmental hazardsAssess life cycle quality factorsDefine design and Performance characteristicsIdentify standardization opportunities6.5.86.5.116.5.126.5.136.5.146.5.156.5.166.5.176.5.186.5.96.5.106.56.5.16.5.26.5.36.5.46.5.56.5.66.5.7Establish designarchitectureProduce integrated datapackageInitiate evolutionary developmentFinalize designDevelop models andFabricate prototypesAssess failure modes,effects, and criticalityAssess testabilityneedsAssess designCapacity to evolve P P P P P P P P P ModelcheckingtoolOutput ofcounterexamplesInputInputInvalidValidDevelopingformulaeEF QAG PQSpecification ofan evaluated targetOutput of checking resultsWorkflowor“Q” may become valid“P” is always validProperties to be satisfiedModeling of statetransitionsModel checkingModelcheckingtoolModelcheckingtoolCounterexamplesFig. 5 Process of Model checking

元のページ 

page 15

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