Formal Design And Verification Of Technical Standard System For Internet Content Rating Service

Internet content rating services are being concerned more and more by government and research institutions, and the development and application of the content rating products are growing. But the current products use their private solutions respectively, and could not be interconnected with each other, which is not conducive to the industrialization and large-scale application of the technology for Internet content rating service. The effective means to resolve the above problem is to develop the technical standard system that is unified, complete and consistent for Internet content rating service.Internet content rating service is the large distributed system that is composed of many functional agents, when be used to accomplish the corresponding business goals, a lot of complex and concurrent interactions among these inner agents will emerged. To ensure that the system functions correctly implemented, the functions of all these agents and the interractions among them must be strictly regulated. But in existing technical standard systems, these functions and interactions are defined and descripted mainly by empirical method, their completeness and consistency have not been fully verified. Therefore, it is necessary to use formal methods to model, design and verify the relevant technical standard system, which in the future can also provide a solid theoretical basis for the detailed designs of all the constituent technical standards and the system development.So, from following four aspects, this thesis carried out research on its technical standard system for Internet content rating service:(1) Constructing the goal model of the business environment formally and extracting the system goals; (2) Extracting all the constituent agents and the corresponding interaction goals among them and specifying them formally; (3) Extracting all the constituent technical standards and the contribution relationship among them and specifying them formally; (4) Verifying the technical standard system formally and comparing the business supporting capabilities of our technical standard system and the other related technical standard systems.The contributions of this thesis include:(1) Constructing the goal model of the business environment formallyThe core business goals have been analyzed, extracted and described formally. Then by refining these business goals step by step, the whole goal model of the business environment has been constructed formally. Finally, the system goals, environment hypothesises and domain properties have been extracted and specified formally. This modeling strategy can theoretically ensure that, supposing the environment hypothesises and the domain properties can be satisfied, the business goals can definitely be accomplished as long as the system goals can be accomplished.(2) Constructing the goal model of the technical standard system formallyBy applying the intermediate states extraction method and the goal refinement method, the whole goal model of the technical standard system has been constructed formally through the step-by-step refinement from the system goals. Then based on all the leaf goals and their responsible agents in this goal model, all the agents that constitue the system have been determined and specified formally, and the corresponding technical standards that specify these agents has been determined. At the same time, based on all the branch goals, all the interactions among the constituent agents have been determined and specified formally, and the corresponding technical standards that specify these interactions have been determined. Finally, based on the refinement relations in this goal model, the contribution relation over the technical standards set has been determined.(3) Completing the formal design of technical standards systemEach technical standard that specifies the fuctional service or the interaction has been given the full description that included the formal specification. From those formal specifications, the information entitiy variables have been extracted, then the corresponding technical standards that will regulate those variables have been determined, and the full descriptions that included the properties of the corresponding information entities have been provided. Then based on the including relation between the formal specifications and the information entity variables, the contribution relation from the set composed by technical standards that specifies the information entity to the set composed by other technical standards has been determined. Finally based on the contribution relation over the technical standards set, the hierarchy of the technical standard system has been determined and described.(4) Proving the completeness and consistency of technical standard system strictlyThe completeness and consistency of this technical standard system has been proved by using formal reasoning, which provides a solid foundation for the detailed designs of its constituent technical standards. At the same time, several basic capabilities of content rating service have been summarized and extracted, and for each basic capability, the standardization support and its negative have been described formally, then our technical standard system and the other existing technical standard systems have been described formally by using the formal descriptions of these basic capabilities. Finally, for our technical standards system and other existing technology standard systems, the complete evaluation results about the capabilities to support all the core business goals of Internet content rating service have been obtained, and the results show that our technical standard system, relative to other existing technology standard systems, can support the business goals of Internet content rating services more completely.This thesis is supported by National Great project of Scientific and Technical Supporting Programs Funded by Ministry of Science & Technology of China During the 11th Five-year Plan.(No.2006BAK11B01) and supported by National Great Project of Scientific and Technical Supporting Programs Funded by Ministry of Science & Technology of China During the 12th Five-year Plan (NO.2011BAK08B05).