Refinement and Validation of Humoral Immunity Based on Event-B

Shi, Xuqing; Zou, Shengrong; Shu, Yudan; Chen, Li

By the outbreak of Covid-19, we should focus more eyesight on the human immune system. Humoral immunity plays an important role in the immunologic mechanism. In this process, B cells and other immune cells cooperate each other to produce antibodies and eliminate antigens by series of interactions, activation, proliferation and differentiation. In this paper, we use the formal language Event-B to model the humoral immunity process on the development tool called Rodin. Humoral immunity process is abstract and has complexity in system design. Accidentally, the formal method is used to verify the correctness and consistency of the complex systems, which is an appropriate approach to model this immunity process by stepwise refinements and validation. We also present an instance to demonstrate the differences between the immunity responses after the invasion of influenza viruses and coronavirus respectively in the last refinement and validate it using proof obligations. Experimental results show that events in our model are all validated by the automatic certification tool on Rodin platform.