Refinement and Validation of the Immune System Based on the Event-B Method

The increasing scale and complex of software makes it difficult to ensure the correctness and consistency of the software, therefore, formal methods emerge and are gradually recognized by industry. This paper introduces the structure and function of the immune cell system, which is a typical large and high-complexity model involving many cytokines and immune responses and how to model the immune system and elaborates the requirements of the immune system in three layers by using the Event-B modeling theory, which is formal languages based on set theory and predicate logic. The model of each layer is verified automatically and manually, which reduces the uncertainty and consistency of the immune system.