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

前言

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

1.相關(guān)理論

1.1 形式化方法

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

1.2 B方法

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.2 形式化B方法的正確性驗證

3．2．1 形式化驗證

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

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

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

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

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

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

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

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

4.結(jié)論

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