Refinement,Validation And Implement Of Immune System Model In Event-B

In the current Internet environment,with the rapid development of social information,more and more industries continue to improve the level of informatization.During the process of preparing for developing a software,it is necessary to analyze the requirements of the system according to the idea of software engineering and figure out the problems which the target system must solve.However,there are inevitable problems in the process of analysis,such as contradictions,ambiguities,incompleteness and confusion of ion levels.The formal method is to ensure that the requirements are not ambiguous through the mathematical specification of the system,and can be verified by mathematical methods to find contradictions and incompleteness in the system,so as to ensure the correctness of the specification.Common formal methods include B method and Event-B method.In this paper,the formal method Event-B was used to develop and simulate the immune system.Rodin tool is used to establish immune system model from requirement rewriting,multiple model refinements to verify obligation proofs in the model,which transits the process of software development to the stage of program design and coding safely and smoothly,to ensure the correctness and consistency in the early stage of software development.The research of the immune system can deepen the understanding of the mechanism in the organism,and the immune system can also provide ideas for the intrusion in the network security and the consistency in the distribution system.This paper takes the immune system as the requirement,adopts the Event-B formal method to establish the immune system model,and then analyzes and verifies the model from requirements on the Rodin platfonn.The system is developed by combining UML and Swing technology,and the main work is as follow:Firstly,describe the immune mechanism in the immune system.According to the modeling process of the Event-B formal method,the immune system in the early generation is created,then carry on the refinements based on the characteristics of each layer of cells,the first-time refinement introduced the concept of cell growth,the second-time refinement introduced the concept of the immune response mechanism,and the third-time refinement introduced the secondary immune response of memory cells,the concept of refining by multiple stepwise refinements,through the multiple refinements to meet all the immune system requirements.Secondly,this paper studies some proof rules,proof tactics and proof types in Rodin platform and demonstrates the process of validation layer by layer in combination with the immune system model.Most of the proof obligations are proved by Rodin's provers,and some of the unfinished proofs are verified by manual certification.Thirdly,after the stage of refinement and validation,the immune system model is analyzed by combining UML and Swing technology and the model has no semantic ambiguity and other problems.Based on the ideas of detailed design in software engineering and Java programming language for coding the corresponding requirements,we realize the immune system with a graphical interface,simulate the process of virus invasion into antibody confrontation visually and count the relationship between the number of cells in different periods in real time.The results of the experiment are consistent with the biological immune response laws,which can be used for simulation teaching by relevant immune system research and learning personnel.In general,based on the process of the formal method,the requirements of the immune system were refined and verified,the refined and verified model was realized by combining UML and Swing technology,and the parameters of the corresponding cells were set for simulation.The results were basically consistent with the laws in biology,and the rationality and usability of the system were verified.