Research On Inf-ProA Model Auto-checking Technology

The modeling of architecture plays an important role in the design of large-scale information system architecture,and model checking is the key to ensure the quality of modeling.In the whole development cycle of such a complex system as Inf-ProA,the architecture plays a guiding role,and the quality of the architecture will largely determine the quality of the developed system.At present,a series of progress has been made in the research of architecture framework,related architecture design tools and model checking technology at home and abroad,but there is little research on the technology of model checking of architecture.Aiming at this problem,this paper carries out the research on the model auto-checking of architecture,including the following contents:(1)Propose an architecture model checking framework based on meta-modelModel checking rules for architectural models contain specific domain knowledge.To be effective,all model checking rules that satisfy the domain knowledge must be considered,which requires considerable time and effort.Canonical model check rule extraction is the basis of effective system verification,but there is not a mature theoretical method about architecture model rule extraction at home and abroad at present.To solve this problem,this paper first defines the definition and classification of the content of the architecture model checking,and then constructs the framework of the architecture model checking based on meta-model,classifies the relationship between the architecture elements,and gives the method of the development of the model checking rules.(2)Extract and define model checking rules for Inf-ProA architectureAccording to the proposed extraction steps of architecture model checking rules,the model is analyzed from IAV and CV viewpoints-two important viewpoints of Inf-ProA,and 21 integrity rules,16 consistency rules and 3 legality rules are extracted and defined,which can basically achieve the full coverage of quality assurance for Inf-ProA architecture modeling scenes.(3)Design and implementation of Inf-ProA architecture model auto-checkingBased on previous extracted checking rules,the model checking function is designed and implemented on the existing architecture design tools,and the model auto-checking of Inf-ProA is realized.