Refinement of the Cytokine Portion of the Immune System Based on Event-B

The Event-B method is a kind of formal software development method, which is mainly used for the functional requirements of the system modeling and validation.The immune system is a large abstract model with high complexity.This paper adopts a new way of thinking,by studying the relationship between immune cytokines and immune cells,the interaction between cells and cytokines in the process of immunity was further explored.At the same time, based on Rodin platform, the formal method Event-B method was adopted, and the top-down strategy was used to refine and verify the immune system model layer by layer.The ideological method of Event-B specification verification was used to solve the problem of high error rate and low efficiency caused by non-formalization in the traditional software design process.