Refinement And Implementation Of The Immune System Using Formal B Method

To meet the increasing development needs of Bioinformatics software and ensure the correctness of the initial requirements of software development,it is necessary to introduce clear requirements documents in the development process.Traditional non-formal sign language without restriction on expression causes blurred linguistic and semantic,to avoid semantic contradictions and logical confusion in development documents,this article introduces formal methods.This approach not only ensures that the semantics of the requirements document are correct,unambiguous,but also ensures the correctness and completeness of the initial specifications of software development.Commonly used formal methods are the B method and the Event-B methodThe immune system is a research hotspot in Bioinformatics.It will be very meaningful if the immune model can be used to master the laws of the immune system.This article uses Event-B to model the immune system.First,it describes the immune requirements,establishes an immune abstract model about immune cytokines and improves the immune model of the CS system,and then uses mathematical methods to verify the obligation of proof in the system The main work of this paper includes the following aspectsFirstly,it is studied that in the traditional software design process,the use of informal methods to analyze requirements will cause the inaccuracy of the development documents,thus introducing formal methods,and the related knowledge of the formal method Event-B is studied.First,the Event-B method is explained.Second,it focuses on the two main components of the Event-B abstract model,Context and Machine,and the relationship between them,the proof obligation and proof rules in the Event-B model,and finally a brief introduction to the modeling platform Rodin tool and UML toolSecondly,the modeling method of Event-B method,which is commonly used in formal methods at the present stage,is studied,and the modeling process of the Event-B formal method,taking the immune system as an example is studied,and then it is added to the model through gradual refinement.Attributes and functions make the system more perfect until all needs are met.First,establish the immune system related to cytokines,introduce the concept of virus division in the first generation model,introduce the concept of cell activation in the first refinement,introduce the concept of immune response in the second refinement,and introduce the concept of cell death in the third refinement.Thirdly,the modeling process of the Event-B formal method,taking the improved CS system as an example is studied.First,an immune abstract model based on the improved CS system is established.The concept of antigen invasion was introduced in the first-generation model,and the concept of information interaction between cells was introduced in the first refinement.The concept of B cell differentiation was introduced in the second refinement,and the concept of immune cells to eliminate antigens and antigen-antibody complexes was introduced in the third refinement.Fourth,it studies how to use the Rodin platform to verify the abstract model and its results.According to the discrete nature of the demand description,this paper uses set theory and logic to generate proof obligations in the Rodin tool and use the prover to verify.Then convert the immune system model verified above into an executable program.Finally,the corresponding classes and functions are established through Java to simulate the entire immune system model.In short,Event-B can accurately verify the semantic correctness and unambiguousness of software requirements.Using Event-B can ensure the accuracy of requirements modeling before software development.This article uses Event-B as a modeling tool to show in detail the entire process of modeling using formal methods,and it also illustrates the importance of specifying requirements before modeling.