key: cord-0058710-folx8sn3
authors: Shi, Xuqing; Zou, Shengrong; Shu, Yudan; Chen, Li
title: Refinement and Validation of Humoral Immunity Based on Event-B
date: 2020-09-24
journal: Proceedings of 2020 Chinese Intelligent Systems Conference
DOI: 10.1007/978-981-15-8450-3_41
sha: 59f84cf219ec308b630b0afc620d465d9d508c2c
doc_id: 58710
cord_uid: folx8sn3

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.

The correctness and security of softwares are always the important topic. Recently, the prevalence of Blockchain technology attracts many scholars and scientists from the field of Computer Science. We know its foundation is smart contract. The hackers put efforts into finding bugs in the code of the contract due to its publicity and this will cause serious accidents [1] . For example, in 2017, a bug happened in smart contract caused the loss of 50 million dollars [2] . In addition, in the field of chain design, the formal validation is equally essential to reduce the risk of large losses. There is an instance that when Intel Corporation published Pentium chains, a zero division error occurred. This code mistake costs Intel Corporation nearly 500 million dollars to retrieve Pentium chains. This accident brought huge economic and reputational losses [3] .

Similar to the introduction above, with the development of the global outbreak of Covid-19, human immunology will be paid more attention. Humoral immunity we concern about is an abstract process occurred among the interactions of diverse immune cells. We use Event-B to model it by stepwise refinements and verify it using proof obligations. Formal method can find amount of bugs and logical mistakes in this procedure. Assume that we validate the correctness of all the states in humoral immunity process, we can realize the software system using traditional programming languages such as java, python and etc. Then, this completed system can be applied for further research in medical community and used as teaching tools in biology classes.

It's well known that when viruses or germ enter the body, the immune system in activated state will response and fight against them. As a result, the immune response which has two main lymphocytes B and T helps to clean the infected cells and the viruses. The response which B cells participate in is also called humoral immunity. For malarial infections, the humoral immunity response tends to be more effective as compared to the cellular immunity responses according to [4] . Tian et al. [5] has been inspired by humoral immunity and created a clustering model to recognize unknown antigens. From 2012 to 2017, authors in [6] [7] [8] [9] have reported various virus dynamic models with humoral immunity or cellular immunity but due to the complexity and abstractness, these models exist drawbacks such as ignoring the absorption effect. The number of lymphocytes involved in immunity is more than 10 12 which exceeds the total number of nerve cells, and the immune system may be more complex than the nervous system. Motivated by the above studies, we consider adopting formal method to model humoral immunity and validate the correctness.

In the process of humoral immunity, antigens are divided into two groups, TD antigens and TI antigens. TD antigens require collisions and touch with phagocytic cells and helper T cells and to be absorbed and treated by them. Then B cells will receive the information from TD antigens and are activated to proliferate and differentiate plamsa cells. Plasma cells will produce the related antibodies to combine with antigens and generate protein precipitation at last. Unlike TD antigens, TI antigens can directly stimulate B cells to secrete plamsa cells in this process. In addition, some activated B cells can change into effector B cells which are also called memory cells during the proliferation and differentiation. When antigens with the same information as before invade the human body, they will discriminate these antigens swiftly and secrete plamsa cells.

Based on the specification of humoral immunity above, we follow the refinement rules to model step by step, which means that the next model after the refinement is to add details based on the previous one. The model of each step is established by the corresponding requirements. At last, we will prove the consistency of this complex systems of immunity process, which means the logics of the model according to our requirements are reasonable.

The following are specific requirements and modeling descriptions. Each circulation in humoral immunity process can follow the same stepwise refinements.

Event-B evolves from classical B language. It supports predicate calculus and theorem proving. It is a formal modeling method based on Action Systems. An Event-B model consists of two basic types of components, namely machine and context [10] . A context describes the static part of a model. In a context, relevant sets, constants, axioms and theorems are defined. On the contrary, a machine is used to describe the dynamic part, which includes relevant variables, invariants and events. An event has its guards and actions [11] . The guards represent the conditions under which the event will be fired. The actions mean what will happen if the event is fired. A context can be 'seen' by a machine, which means that the machine will use the static elements defined in the context [12] . The fundamental knowledge will be used in the following parts.

As shown in Table 1 , we specific the requirements of the initial model. Briefly speaking, it describes the growth of B cells which is from pre-B cells to native B cells. Only native B cells can be interacted with other immune cells [13] . Then we start to model it.

Machine m0 is created which sees c0. M0 includes four events and we will introduce the main three of them. But before that, we need to define variables and the related invariants. As shown in Table 2 , there are four variations. It is shown that cell which simulates a set of all the cells in the human body is contained in carrier set Cell defined in c0 and cell can partition into bcell(other cell sets will be joined in the next machines). Bcell hp and bcell state are all total surjections which denotes that one of the values of Hp and one State can correspond to multiple B cells and their domains and ranges are certainly equal to the sets revealed in the functions.

The following are events. In Fig. 1 .(a), we can see the code of the event new bcell. Bcellobj is a formal parameter which denotes a B cell. Two guards are constrained conditions. Grd1 is the constrained condition which means that bcellobj is not the element of bcell. If grd1 is satisfied, then take actions. Act1 and act4 merge bcellobj into bcell and cell respectively. Then act2 assigns initialHp to the value of Hp of bcellobj and act3 assign prophaseState to the cell state of it. Then, we will introduce bcell grow to immatureState in Fig. 1.(b) . In this event, the formal parameter is bcellobj. Guards constrain that bcellobj must satisfy some conditions. When satisfying these guards, take act1 to change the state into immatureState.

As shown in Table 1 , we add the details of the process which describes how TD antigens and TI antigens stimulate B cells to activation respectively and it is divided into four steps. Then, we establish the model. We establish m1 which sees c1 and refines m0. There are six events in m1 and we will concretely state three of them. As shown in Table 3 , we define related variables and invariants. Cell, ag and aginfo are subsets of their parallel carrier sets in c1 and they have their corresponding elements which have slave relations with them according to the associated invariants. Td ag td aginfo and tiag tiaginfo are both total surjections which denote that each TD antigen and TI antigen have their linked DNA information so domains are td ag and tiag and ranges are td aginfo and tiaginfo respectively. Mngcell td aginfo, helperTcell td aginfo, bcell td aginfo and bcell tiaginfo are partial functions because their domains are changeable that cells are constantly produced and dead in the human body and not each phagocyte cell, helper T cell or bcell has opportunity to carry DNA information of antigens.

The following are events. The event new td ag has two formal parameters, td agobj and td aginfoobj. Grd1 and grd2 respectively constrain that they are not the elements of the linked sets. When grd1 and grd2 are contented, then take actions. Act1 and act2 merge them into the related sets. Act3 indicate that the antigen DNA information which td agobj carries is assigned to td aginfoobj. In Event-B method, function is not only relation but also set [14] . The event next event has three formal parameters, td agobj, mngcellobj and td aginfoobj. Grd1 and grd2 regulate their slave relations. Grd3 denotes that td aginfoobj is the value of td adobj under he map function. Grd4 restricts that mngcellobj is not in the domain of mngcell td aginfo because before this event is carried out, mngcellobj doesn't take any information. When act1 are permitted to take, mngcellobj will carry td aginfoobj. 

As shown in Table 1 , the details of the process which describes how the activated B cells change into plasma cells and produce antibodies are added into the previous model. In addition, the appearance of memory cells will work soon. The second refinement requirements are divided into three steps. After stating the requirements, we will complete modeling. We describe the dynamic machine m2. Similar as before, in Table 4 , we define the variables plasmacell, memorycell, ab, td ab and ti ab, which imply the sets of these kinds of cells in the actual human body and the relevant invariants regulate the slave relations among them. Plasmacell td aginfo, plasmacell ti aginfo and etc. are all partial surjections because the entire cells in them are directly or indirectly produced by the B cells which have DNA information of antigens and they will also carry it. Thus, the domains are equal to their correlated cell sets. But doubtfully, B cells will not take all kinds of antigen information so the range is included by td aginfo or ti aginfo.

Later, we will state the two main events. The first event specifies the process that B cells with DNA information of TD antigens proliferate and differentiate. B cells will mostly change into plasma cells, and a little portion of them will translate into memory cells. To simulate this process, we set seven formal parameters in the event as before. Guards constrain that td aginfoobj is carried by bcellobj, and plasma cells and memorycellobj are not produced before taking actions. Hence, they are not the elements of the relevant cell sets. When satisfying guards, bcellobj disappears to change into plasma cells and memorycellobj. In addition, the new produced cells carry the antigen information. The second event new td ab imitates the process of producing antibodies whose goal is to eliminate TD antigens. Formal parameters are td abobj, plasmacellobj and td aginfoobj. Guards regulate them. When guards are contented, td abobj is truely produced so it will join the set and it will carry the DNA information of the related antigens.

As shown in Table 1 , this refinement consists of two procedures. One is that memory cells discriminate the antigens which the ones of the same type invaded before and they secret plasma cells to produce antibodies. The other is that antibodies combine with antigens and induce immunological effects. Subsequently, we start to build up the model. In this refinement, we didn't append novel elements in the static context so we just need to create dynamic machine m3 which sees c2. In Table 5 , we define the new entrants. Memorycell td ag and memorycell ti ag are both total functions which imply the interactions between the memory cells and antigens. Then, we introduce the events. The first event specifies how memory cells indentify TD antigens. When guards are all satisfied, act1 will be taken that 'memorycellobj →td agobj' will be integrated into memorycell td ag. After that, We describe the immune responses during the process of combining antibodies with TD antigens. In this event, grd1 to grd4 make sure that they both belong to the related sets and possess antigen information. Grd5 to grd8 regulate that td abobj and td agobj carry the same type of DNA information of antigens. After fulfilling the guards, we take ac1 and act2 to extract td abobj and td agobj from the related sets because immune responses happen between them and they are combined and changed into precipitate.

As shown in Table 1 , in the last refinement, for further research on Covid-19, we present an instance to specify the differences of the immune responses between normal influenza viruses and coronavirus when they invade human bodies [15] [16] [17] . This refinement includes five steps in the table. Then, we introduce our designed model. We build up the dynamic machine m4. As usual, we specify the variables and their invariants in Table 6 . Virus, virusinfo and their internal elements are defined as same as ones in c4. In virus in virusinfo and co virus co virusinfo are both total surjections because each virus has DNA or RNA information and each kind of virus information can correspond to multiple viruses. Bcell in virusinfo, memorycell in virusinfo, bcell harmless cellinfo and memorycell harmless cellinfo are all partital functions because not each bcell or memory cell got in touch with viruses or harmless cells and carry their information. For that, domains and ranges of these functions are included by the relevant sets. Upp cell state and pul cell state are both partial surjections because each upper respiratory tract cell or pulmonary cell has a cell state(alive or dead), so their domains are certain.

After elaborating the variables and invariants, we can characterize the events. The event new in virus has two parameters and guards constrain that they are not the elements of the related sets before taking actions. When guards are satisfied, the two parameters will be combined into the sets. Finally, we introduce the event which describes how coronavirus avoid the examination from B cells or memory cells, and then cause fatal damage to the upper respiratory tracts cell, pulmonary cells and other useful cells which are playing important roles. This event has four parameters, which are bcellobj, co virusobj, upp cellobj and pul cellobj. Grd1 and grd2 represent that bcellobj is in activeState so it has abilities to receive virus information and indirectly produce antibodies to fight against viruses. Grd5 to grd8 constrain that upp cellobj and pul cellobj are regularly working in the human body. The most important guard is grd4. This guard imitates that when bcell collides with co virusobj, it receives its information but this information is wrong which is mocked by co virusobj. Consequently, it can be reckon as DNA information of the harmless cells and bcellobj will not handle it. When these guards are passed, co virusobj will do harm to upp cellobj and pul cellobj. Therefore, act1 and act2 assign deadState to them to show the consequences.

Rodin is a complex tool platform which supports the application of the Event-B formal method. It provides core functionality for syntactic analysis and proofbased verification of Event-B models. The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof [18] . We utilize the automatic proof plugin on Rodin to validate our established model and the events which cannot be automatically verified are proved manually. In Fig. 2 , we display the results. In Fig. 2.(a) , there are a total of 16 proof obligations in the initial model and 10 obligations of them are automatically verified. For the left 6 ones, we add some constrained conditions and hypotheses to make the obligations pass through the validation. In Fig. 2.(b) , there are a total of 41 proof obligations in the first refinement model and they are all validated automatically. In Fig. 2.(c) , there are a total of 34 proof obligations in the second refinement model and they are all validated automatically. In Fig. 2.(b) , there are a total of 28 proof obligations in the third refinement model and they are all validated automatically. In Fig. 2.(b) , there are a total of 41 proof obligations in the last refinement model and they are all verified by the automatic plugin.

In this paper, we extract requirements from the abstract process of humoral immunity and show an instance which reflects on the differences between the methods of the attacks which aim at harming the human bodies from influenza viruses and coronavirus. This instance is our try to hope to help push the research on Covid-19. Then, based on the requirements, we define models by stepwise refinements and prove its correctness and consistency. However, we know this is just a portion of the enormous and complex immune system. Thus, we will do further research and develop the superb system. In the future, we also want to use real data to validate our Event-B model to increase its rationality.

Develop leave application using blockchain smart contract

Generative adversarial networks based on edge computing with blockchain architecture for security system

An interval-based approach to modelling time in Event-B

Immunology of malaria

A clustering model inspired by humoral immunity

Global stability properties for a delayed virus dynamics model with humoral immunity response and absorption effect

Global stability of in-host viral models with humoral immunity and intracellular delays

Stability and Hopf bifurcation for a virus infection model with delayed humoral immunity response

Global stability analysis of humoral immunity virus dynamics model including latently infected cells

Towards transformation from UML to event-B

Formal modeling of the simple text oriented messaging protocol using Event-B method

Modeling in Event-B: System and Software Engineering

Finding an effective distance between T-cell and B-cell using S/W ARQ in an immune system communication

Formal modelling of cruise control system using Event-B and Rodin platform

Identifying discriminative amino acids within the hemagglutinin of human influenza A H5N1 virus using a decision tree

The role of imaging in the detection and management of COVID-19: a review

Using microfluidics to investigate tumor cell extravasation and T-cell immunotherapies

Event-B patterns and their tool support