Design And Development Of Immune System Based On Event-B

With the increasing scale of computer software system,the complexity of the system is also promoting,and the potential problems in the design will affect the security and reliability of the software system.Traditional software engineering methods have been difficult to meet the current complex and security requirements,it is an urgent need to adapt to the current development and need more methods to develop software with higher security and large complex system with lower cost.In order to solve the above problems,Unified Modeling Language(UML)is widely used in software development and design.UML is a semi-formal graphic modeling language,it describes the system by clear visual graphics,which facilitate communication and understanding between the graphical software codes.UML has now become the standard of software industry in object-oriented analysis and design.However,UML semantic part adopts the informal natural language,which is short of precise semantics and leads to the inaccurate description of complex large-scale software system,prone to fuzziness and ambiguity.It is not convenient for users to establish strict requirements model and use automated tools to describe in the statute for consistency check,analysis and verification.There is a lot of synergies between formal methods and UML.The strict mathematical definition of formal method can make up for the deficiency of UML in semantics,and can make consistency check and correctness analysis of UML modeling result and requirement description.At the same time,UML can reduce the difficulty of system development by using formal methods directly,and enhance the practical application value of formal methods in system development.The combination of UML and formal methods is of great significance to improve the reliability and security of software.In order to detect and correct errors timely in development,reduce development costs,verify and standardize software systems and properties in a precise and concise manner,on the basis of analyzing the characteristics of UML model diagram,in this paper,Event-B formal method is selected as the formal specification method for the UML model diagrams of the complex and nonlinear immune system.The main works are as follows:1.The basic concepts of UML and the application background which is often used to solve the problems of object-oriented modeling are briefly described.The advantages of UML to facilitate communications and support the whole lifecycle of software development are introduced.And it is pointed out that the UML lacks precise semantic definition and the descriptions of the software structure can only stay on the level of non-formalization.Aiming at this problem,this paper puts forward to the Event-B formal method combined with UML,the Event-B method makes up for the informal semantic definition of UML based on its rigorous mathematical theory,and the Rodin tool of Event-B method has its own proof obligation generator which can make up for the lack of verification tools in UML model diagrams.2.The operating mechanism of the immune system in the body is studied,and the requirement to establish the model is obtained.Establishing clear and intuitive model diagrams based on the UML,and the functions of the immune system are described in detail from the static and dynamic aspects of the system.The Event-B method is used for formal analysis and specification of the model,and the refinement strategy is adopted to add behavioral rules and consummate functions to the immune system.The model checking and theorems of the formalized method of Event-B can guarantee the consistency and correctness of the immune system and the requirements,which improving the reliability of the immune system.3.Modeling,analysis and verification of the system based on UML and Event-B Model,the immune system is transformed into executable code designed by the UML and Event-B formal method using the Java programming language,and the relevant parameters of influenza virus are set to the immune system.After running the established immune system,the system will generate a graph of the movement and collision of the cells involved and display a graph of the real-time number of each cell.The experimental results obtained from the system model are consistent with the biological immune response law,which validates the rationality of the system.