?:abstract
|
-
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 © 2021, The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd
|