基于形式化B方法的因子網(wǎng)絡(luò)模型構(gòu)建探討

揚(yáng)州市職業(yè)大學(xué)信息工程學(xué)院 沈 利

前言

在生物研究領(lǐng)域，因子網(wǎng)絡(luò)始終是研究的熱點(diǎn)。雖然很多研究學(xué)者對(duì)其進(jìn)行了深入的研究，也取得了較為理想的效果，但是仍舊有些問題沒有解決。比如細(xì)胞因子的作用機(jī)理及過程等問題。這就要求研究學(xué)者將計(jì)算機(jī)技術(shù)用于因子網(wǎng)絡(luò)研究中，通過計(jì)算機(jī)進(jìn)行因子網(wǎng)絡(luò)模型的構(gòu)建，模擬的因子網(wǎng)絡(luò)調(diào)控圖，了解細(xì)胞因子的作用機(jī)理及過程，為生物研究提供新的方向。因此，基于形式化B方法的因子網(wǎng)絡(luò)模型構(gòu)建分析具有一定的理論價(jià)值。

1.相關(guān)理論

1.1 形式化方法

形式化方法主要是應(yīng)用數(shù)學(xué)方法進(jìn)行目標(biāo)軟件系統(tǒng)屬性全面描述的一種方法。形式規(guī)約是形式化方法的核心研究?jī)?nèi)容，作為形式化方法設(shè)計(jì)以及程序編輯的基礎(chǔ)，能夠驗(yàn)證目標(biāo)軟件程序的正確性。一般來說，形式規(guī)約主要有兩種方法：其一，基于模型的形式規(guī)約，主要是通過目標(biāo)軟件系統(tǒng)的計(jì)算模型進(jìn)行系統(tǒng)行為的描述；其二，基于性質(zhì)的形式規(guī)約，主要是通過對(duì)系統(tǒng)必須滿足某些性質(zhì)的定義實(shí)現(xiàn)目標(biāo)軟件系統(tǒng)的描述。

1.2 B方法

在形式化方法中，應(yīng)用最為廣泛的就是B方法，可以用于實(shí)時(shí)、仿真以及信息處理工程。從本質(zhì)角度看來，B方法主要進(jìn)行軟件生存周期重要內(nèi)容的處理，通過相關(guān)步驟的設(shè)計(jì)，實(shí)現(xiàn)層次性結(jié)構(gòu)和能夠執(zhí)行代碼的生成。在B方法中，涉及到的所有事項(xiàng)都會(huì)對(duì)數(shù)學(xué)證明造成影響，也就是說，B方法中的證明可以反映出目標(biāo)軟件系統(tǒng)的準(zhǔn)確程度。B方法中最為重要的機(jī)制是抽象機(jī)，抽象機(jī)是B語(yǔ)言中的模塊，主要是指數(shù)據(jù)和數(shù)據(jù)上實(shí)施的操作。抽象機(jī)主要包括規(guī)格說明級(jí)、實(shí)現(xiàn)級(jí)以及精化級(jí)這三種類型。

另外，B方法具備較為突出的規(guī)范性特征，主要表現(xiàn)為數(shù)據(jù)規(guī)范化以及操作規(guī)范化這兩種。其中，數(shù)據(jù)規(guī)范化是指在進(jìn)行抽象機(jī)的數(shù)據(jù)描述時(shí)，會(huì)使用規(guī)范化的數(shù)學(xué)概念，比如函數(shù)、集合或者序列，這些數(shù)學(xué)概念都會(huì)遵循特定條件定義的不變式法則；操作規(guī)范化是指在進(jìn)行抽象機(jī)的操作描述時(shí)，會(huì)使用偽代碼，偽代碼會(huì)將抽象機(jī)的操作描述為前條件以及原子動(dòng)作這兩種，只有操作完全滿足前條件時(shí)，才能夠執(zhí)行，原子動(dòng)作是指廣義替換方法實(shí)施的形式化，可以為模型的精化步驟奠定良好的基礎(chǔ)，精化步驟可以提高代碼的規(guī)范化以及正確性。

1.3 因子網(wǎng)絡(luò)

人體的免疫系統(tǒng)作為免疫應(yīng)答的基礎(chǔ)，主要負(fù)責(zé)執(zhí)行機(jī)體的免疫功能，能夠幫助人體抵御外界的病毒。免疫系統(tǒng)包含的層次網(wǎng)絡(luò)被稱作因子網(wǎng)絡(luò)，和神經(jīng)網(wǎng)絡(luò)有所不同，神經(jīng)系統(tǒng)具備較為顯著的網(wǎng)絡(luò)結(jié)構(gòu)特征，突起的神經(jīng)細(xì)胞連接為神經(jīng)系統(tǒng)提供了網(wǎng)絡(luò)結(jié)構(gòu)基礎(chǔ)。但是免疫因子并沒有直接連接的網(wǎng)絡(luò)結(jié)構(gòu)，該網(wǎng)絡(luò)主要從功能的角度出發(fā)，對(duì)免疫因子的的作用狀況進(jìn)行描述。因子網(wǎng)絡(luò)主要包括免疫細(xì)胞和細(xì)胞因子這兩部分，細(xì)胞因子主要是指機(jī)體在免疫應(yīng)答或者炎癥中，具備調(diào)節(jié)和效應(yīng)功能的蛋白或者小分子多肽，又被稱作淋巴因子或者單核因子[1]。

2.因子網(wǎng)絡(luò)模型的構(gòu)建

2.1 因子網(wǎng)絡(luò)模型的分類

首先，IMMSIM模型。IMMSIM會(huì)通過自動(dòng)機(jī)進(jìn)行特別約定的加強(qiáng)，比如，執(zhí)行規(guī)則屬于概率事件，會(huì)受到引入隨機(jī)數(shù)的影響；柵格的位置中包括一定數(shù)量的個(gè)體，這些個(gè)體有屬于自己的位置，也可以進(jìn)行位置的移動(dòng)。IMMSIM模型主要按照如下流程進(jìn)行免疫應(yīng)答的模擬：

在該模型中，首先要注入兩次抗原分子，進(jìn)行系統(tǒng)變化狀況的觀察，并在柵格的每一個(gè)個(gè)體的位置上注入一定量的免疫細(xì)胞以及分子，確保免疫細(xì)胞以及分子保持初始狀態(tài)；再在某一個(gè)時(shí)刻進(jìn)行抗原的注入，將一步范圍內(nèi)的所有個(gè)體位置進(jìn)行隨機(jī)交換，這時(shí)有些免疫細(xì)胞以及分子會(huì)死亡，也會(huì)有新的免疫細(xì)胞以及分子出生；最后，出生的免疫細(xì)胞以及分子會(huì)擴(kuò)散到其余位置，按照這一流程循環(huán)。在模型循環(huán)的過程中，有些B細(xì)胞能夠分泌出抗體，并參與細(xì)胞的高頻變異，從而獲得較高的識(shí)別度；當(dāng)某些B細(xì)胞的親和力滿足一定標(biāo)準(zhǔn)時(shí)，可以進(jìn)行相同抗原的注入，從而進(jìn)行免疫二次應(yīng)答。但是因?yàn)橛洃浖?xì)胞可以在短時(shí)間內(nèi)識(shí)別出抗原模式，所有抗原很快就會(huì)被消滅。

然后，基于Multi-Agent構(gòu)建的免疫模型。Multi-Agent和人體免疫系統(tǒng)在很多方面十分相似，具體有以下幾方面：其一，兩者均由自治實(shí)體所組成，在Multi-Agent系統(tǒng)和人體免疫系統(tǒng)中，均具備一定的自治性；其二，兩者均具有個(gè)體目標(biāo)以及全局目標(biāo)，對(duì)于人體免疫系統(tǒng)而言，個(gè)體目標(biāo)是通過識(shí)別抗原實(shí)現(xiàn)生存，全局目標(biāo)是將抗原消滅掉；其三，具備學(xué)習(xí)的能力，人體免疫系統(tǒng)能夠進(jìn)行免疫調(diào)節(jié)以及記憶，Multi-Agent系統(tǒng)具備學(xué)習(xí)算法；其四，可調(diào)性，兩者都可以根據(jù)周圍環(huán)境的變化進(jìn)行相應(yīng)的調(diào)整，個(gè)體具備交流能力；其五，兩者需要由一定的機(jī)制控制整個(gè)系統(tǒng)，人體免疫系統(tǒng)通過克隆選擇算法控制，Multi-Agent系統(tǒng)通過決策過程以及學(xué)習(xí)算法控制。基于上述相似之處，基于Multi-Agent系統(tǒng)構(gòu)建的免疫模型可以用于因子網(wǎng)絡(luò)模型的構(gòu)建。

2.2 形式化B方法與因子網(wǎng)絡(luò)模型的結(jié)合

通過上述分析可知，IMMSIM模型主要通過免疫應(yīng)答進(jìn)行免疫系統(tǒng)功能的描述，但是存在一定的局限性，除了免疫應(yīng)答以外的免疫系統(tǒng)沒有進(jìn)行刻畫；基于Multi-Agent構(gòu)建的免疫模型不能從時(shí)間角度進(jìn)行因子網(wǎng)絡(luò)的調(diào)控，也存在一定的局限性。為了彌補(bǔ)這兩種模型的不足，本文提出了基于形式化B方法的因子網(wǎng)絡(luò)模型，構(gòu)建了IMMUNE-B模型。因?yàn)樾问交疊方法在人工生命以及生物工程等多個(gè)領(lǐng)域有非常廣泛的應(yīng)用，發(fā)揮著十分重要的作用，而且大部分軟件都能夠支持形式化B方法。所以進(jìn)行因子網(wǎng)絡(luò)這類復(fù)雜程度較高網(wǎng)絡(luò)的描述，形式化B方法是非常合適的選擇。

基于形式化B方法構(gòu)建的因子網(wǎng)絡(luò)模型可以看做是，將免疫因子網(wǎng)絡(luò)移動(dòng)到抽象空間內(nèi)，在這一空間內(nèi)實(shí)現(xiàn)免疫因子網(wǎng)絡(luò)的模擬。這種模擬方法不僅可以展示出模擬的結(jié)果，還能夠展現(xiàn)因子網(wǎng)絡(luò)的動(dòng)態(tài)過程，可以從時(shí)間角度進(jìn)行因子網(wǎng)絡(luò)的調(diào)控，從而發(fā)現(xiàn)因子網(wǎng)絡(luò)中各個(gè)因子的作用規(guī)律，為正確因子網(wǎng)絡(luò)模型的構(gòu)建奠定良好的基礎(chǔ)。IMMUNE-B模型的構(gòu)建目的在于通過計(jì)算機(jī)進(jìn)行因子網(wǎng)絡(luò)中所有細(xì)胞活動(dòng)過程的模擬，了解細(xì)胞因子和抗原間的關(guān)系與作用過程。在IMMUNE-B模型中，用戶能夠根據(jù)模型系統(tǒng)的定義，自行選擇注入細(xì)胞和抗原的種類，使系統(tǒng)進(jìn)入初始化狀態(tài)；然后在規(guī)定的時(shí)間內(nèi)，觀察系統(tǒng)運(yùn)行所得的結(jié)果；最后，系統(tǒng)可以將因子網(wǎng)絡(luò)中各因子的函數(shù)曲線圖，工作人員可以根據(jù)系統(tǒng)數(shù)次運(yùn)行的結(jié)果，得出因子網(wǎng)絡(luò)的某些規(guī)律[2]。

3.基于形式化B方法的因子網(wǎng)絡(luò)模型構(gòu)建

3.1 系統(tǒng)的分析與描述

因子網(wǎng)絡(luò)模型構(gòu)建的目的是進(jìn)行免疫因子網(wǎng)絡(luò)調(diào)控圖運(yùn)行狀況的模擬，以此掌握因子網(wǎng)絡(luò)調(diào)控過程中所有量的變化狀況和調(diào)控圖的穩(wěn)定情況，了解初始條件會(huì)對(duì)因子網(wǎng)絡(luò)調(diào)控產(chǎn)生什么影響。為了提高模型描述的準(zhǔn)確性，需要應(yīng)用形式化B方法進(jìn)行因子網(wǎng)絡(luò)模型的形式化描述。一般來說，因子網(wǎng)絡(luò)模型包括細(xì)胞、因子、抗原以及抗體這四個(gè)實(shí)體，細(xì)胞主要分為七個(gè)子類別，每種細(xì)胞都要進(jìn)行標(biāo)識(shí)、位置、顏色、年齡以及大小這五種屬性的描述，記錄細(xì)胞從出生到死亡的全過程；因子包括九個(gè)子類別，每種細(xì)胞因子發(fā)揮的作用有所不同的，但是擁有共同的作用對(duì)象，即細(xì)胞與抗原，細(xì)胞因子可以促進(jìn)細(xì)胞生長(zhǎng)與活化，可以抑制抗原的復(fù)制；抗原主要用于刺激免疫細(xì)胞，促使細(xì)胞進(jìn)行活化，產(chǎn)生免疫因子，而免疫因子又會(huì)對(duì)細(xì)胞和抗原產(chǎn)生作用；抗體是指效應(yīng)B細(xì)胞分泌的物質(zhì)，能夠?qū)⒖乖苯託⑺馈?/p>

在因子網(wǎng)絡(luò)模型中，工作人員需要對(duì)系統(tǒng)進(jìn)行如下描述：第一，細(xì)胞分泌的因子種類以及因子的作用需要符合生物學(xué)描述的內(nèi)容；第二，系統(tǒng)運(yùn)行的條件是一定要有抗體、T細(xì)胞以及B細(xì)胞的進(jìn)入；第三，只有細(xì)胞受到抗原的刺激，才可以進(jìn)行活化，從而產(chǎn)生細(xì)胞因子；第四，細(xì)胞的分裂和死亡需要滿足一定的條件。

另外，因子網(wǎng)絡(luò)模型中形式化B方法的描述需要做到以下幾點(diǎn)：第一，機(jī)器Cell，能夠進(jìn)行細(xì)胞類的封裝，模型系統(tǒng)需要對(duì)CELL（表示現(xiàn)在或者未來的細(xì)胞）、CATEGORY（表示細(xì)胞的類別）以及STATUS（表示細(xì)胞的狀態(tài)）這三個(gè)集合進(jìn)行定義，定義的內(nèi)容為細(xì)胞的七個(gè)子類別以及五種屬性；第二，機(jī)器Cytokine，能夠進(jìn)行細(xì)胞因子屬性與操作的封裝，模型系統(tǒng)需要對(duì)CYTOKINE以及CATEGORY這兩個(gè)集合進(jìn)行定義，定義的內(nèi)容為因子的九個(gè)子類別；第三，機(jī)器Virus，這一程序的描述與機(jī)器Cell相似，主要用于抗原的封裝，只需要定義VIURUS一個(gè)集合即可；第四，機(jī)器antibody，能夠進(jìn)行抗體的封裝，只需要定義ANTIBODY一個(gè)集合即可[3]。

3.2 形式化B方法的正確性驗(yàn)證

3．2．1 形式化驗(yàn)證

就目前的研究狀況而言，因子模型的形式化驗(yàn)證方法主要有模擬測(cè)試方法、模擬監(jiān)測(cè)方法以及演繹驗(yàn)證方法。其中，模擬測(cè)試方法是通過實(shí)驗(yàn)的手段進(jìn)行系統(tǒng)的查錯(cuò)，工作人員需要進(jìn)行多組數(shù)據(jù)輸入，然后對(duì)數(shù)據(jù)的輸出結(jié)果以及運(yùn)行過程進(jìn)行檢查與分析，從而找出系統(tǒng)中存在的錯(cuò)誤，這種驗(yàn)證方法只能夠證明系統(tǒng)的錯(cuò)誤，卻不能證明系統(tǒng)的正確，應(yīng)用具有一定的局限性。

模擬監(jiān)測(cè)方法主要是在有限狀態(tài)系統(tǒng)空間內(nèi)實(shí)施窮盡搜索，工作人員會(huì)應(yīng)用形式化語(yǔ)言或者遷移系統(tǒng)實(shí)現(xiàn)系統(tǒng)的模擬，再通過時(shí)態(tài)邏輯或者模態(tài)邏輯實(shí)現(xiàn)系統(tǒng)期望性質(zhì)的全面描述，最后應(yīng)用算法在有窮步的范圍內(nèi)進(jìn)行系統(tǒng)的檢測(cè)，檢測(cè)系統(tǒng)是否能夠滿足期望性質(zhì)。這種方法的檢測(cè)結(jié)果對(duì)待檢測(cè)系統(tǒng)有高的依賴性，如果待檢測(cè)系統(tǒng)較為復(fù)雜，很容易出現(xiàn)空間爆炸現(xiàn)象。

演繹驗(yàn)證方法主要是通過公理與推導(dǎo)規(guī)則實(shí)現(xiàn)待檢測(cè)系統(tǒng)的驗(yàn)證，支持無線狀態(tài)系統(tǒng)的驗(yàn)證。但是這種方法對(duì)操作者的要求比較高，操作者需要具備較強(qiáng)的邏輯推理能力以及相關(guān)經(jīng)驗(yàn)。

3．3．2 系統(tǒng)驗(yàn)證

在上文中，本文對(duì)系統(tǒng)的描述進(jìn)行了分析，為了保障描述的四種機(jī)器具備較高的準(zhǔn)確度，需要對(duì)其進(jìn)行正確驗(yàn)證。筆者主要選用演繹驗(yàn)證法進(jìn)行機(jī)器的驗(yàn)證。對(duì)于形式化B方法，每個(gè)代碼生成的步驟都需要進(jìn)行驗(yàn)證，從而保證系統(tǒng)的準(zhǔn)確性。在系統(tǒng)驗(yàn)證過程中，首先要進(jìn)行類型檢查，檢查對(duì)象為四種機(jī)器涉及到的所有集合論結(jié)構(gòu)謂詞；然后再進(jìn)行證明義務(wù)，如果機(jī)器的證明義務(wù)是正確的，就表明該機(jī)器通過了系統(tǒng)驗(yàn)證，可以投入使用。

3.3 系統(tǒng)的模擬運(yùn)行

在上述分析的基礎(chǔ)上，本文采用具體的程序語(yǔ)言對(duì)基于形式化B方法的因子網(wǎng)絡(luò)模型進(jìn)行了模擬仿真以及運(yùn)行分析。在模擬仿真過程中，本文首先進(jìn)行系統(tǒng)對(duì)象管理類的定義，負(fù)責(zé)多種對(duì)象的管理，如細(xì)胞、因子、抗原和抗體；然后進(jìn)行了動(dòng)畫控制類的定義，作為對(duì)象管理類以及圖形界面的連接橋梁；最后，圖形界面，工作人員可以在該界面中進(jìn)行對(duì)象參數(shù)以及系統(tǒng)參數(shù)的設(shè)置，細(xì)胞、因子、抗原和抗體的所有實(shí)時(shí)曲線圖都可以通過界面展示。模擬的仿真系統(tǒng)流程如下：開始→初始化→啟動(dòng)畫面→動(dòng)畫結(jié)束→碰撞檢測(cè)→更新畫面→結(jié)束。在初始化以后，可以進(jìn)入系統(tǒng)的仿真程序，系統(tǒng)在正常運(yùn)行的過程中，按照系統(tǒng)體現(xiàn)細(xì)胞的生長(zhǎng)過程、分裂過程以及死亡過程，細(xì)胞能夠分泌細(xì)胞因子；抗原能夠刺激細(xì)胞，從而促使細(xì)胞活化以及抗體可以殺死抗原等條件，提高系統(tǒng)模擬的真實(shí)性。

觀察系統(tǒng)模擬運(yùn)行的結(jié)果，工作人員可以根據(jù)系統(tǒng)給出的曲線圖進(jìn)行細(xì)胞、因子、抗原和抗體數(shù)量的記錄，了解因子網(wǎng)絡(luò)模型運(yùn)行的結(jié)果差距；還可以在抗原數(shù)量為0時(shí)，觀察細(xì)胞、因子和抗原的數(shù)量變化，從而掌握基于形式化B方法的因子網(wǎng)絡(luò)模型的有效性[4]。

4.結(jié)論

綜上所述，形式化B方法在生物學(xué)領(lǐng)域中有其獨(dú)有的優(yōu)勢(shì)，能夠促進(jìn)生物學(xué)的發(fā)展。通過本文的分析可知，通過形式化B方法進(jìn)行因子網(wǎng)絡(luò)的描述，是將嚴(yán)格的數(shù)學(xué)作為基礎(chǔ)，能夠在很大程度上提高因子網(wǎng)絡(luò)模型的正確性，使研究學(xué)者通過因子網(wǎng)絡(luò)模型找出生物學(xué)規(guī)律，從而使生物學(xué)取得進(jìn)一步的發(fā)展。希望本文可以為研究學(xué)者進(jìn)行因子網(wǎng)絡(luò)模型的構(gòu)建提供幫助。

[1]沈利．UML類圖與形式化B方法相結(jié)合的應(yīng)用研究[J]．信息技術(shù)與信息化,2017(11)∶117-119．

[2]沈利．基于B方法的UML模型形式化轉(zhuǎn)換的應(yīng)用研究[J]．信息技術(shù)與信息化,2017(10)∶90-92．