Research On Immune System Model Based On Event-B Formal Method

In nowadays society,with the rapid development of social information,every industry is closely connected to software.To develop software,the first thing to do is to analyze the software requirements,and in the description process we can't avoid grammatical or semantic errors.For free of avoiding the loss which is due to these unnecessary mistakes,formal method emerges.Currently,there are two common methods in the field of formal methods which called B method and Event-B method.These two methods are formal system languages ground on set theory and predicate logic.The Event-B method evolve from the B method and has hugeness preponderance that the B method does not have.Moreover,Event-B method has great superiority on the tool platform which called Rodin Platform.Rodin platform provides a system-level development mode for the Event-B method.The required attributes and functions can be added to the model by means of stepwise refinement.In addition,Rodin platform simplifies the verification process of Event-B method,and it provides multiple automatic provers,supporting more proof obligations.At the same time,it minimizes the impact on changing existing proofs,and provides effective support for model refinement and proof.This paper takes the immune system as the development requirement,using the Event-B method to establish the abstract model of the immune system software,and then elaborating on the entire process from demand analysis to verification of the model under the Rodin platform.The main work is as follow:Firstly,this paper studies the present common formal methods,B method and Event-B methods,and their respective modeling methods.It introduces the development process of B method and analyzing its advantages and disadvantages.On this basis,Event-B method is put forward to improve the disadvantages of B method,especially the part of refinement method and interactive proof.Finally,a summary is made to compare the two methods.Secondly,this paper takes immune system as an example to introduce the modeling process of the Event-B formal method.An abstract model of the immune system is created,and then gradually added tree attributes or functions of the system to the model with refinement skills in order to expand the model until all needs are metThirdly,this paper studies the Event-B model validation based on the Rodin platform,stating the proof obligations and the provers related to the model validation,then demonstrating the reasoning process.Finally,the whole model's proof is finished by interactive proof.In general,the Event-B formal method can help developers to verify the accuracy and consistency of software system requirements.In this paper,the abstract model of immune system is established based on the Event-B method,and the whole process from requirement rewriting to model validation is demonstrated in detail,which reflects the importance of using formal method in the early stage of software development.