基于B方法的流量控制系統(tǒng)的實(shí)現(xiàn)

【摘要】 通過對形式化B方法的研究，結(jié)合網(wǎng)絡(luò)流量控制系統(tǒng)模型，討論了該模型在形式化B方法下的具體應(yīng)用，給出了該系統(tǒng)的抽象機(jī)模型和精化過程。

【關(guān)鍵詞】 B方法;流量控制;特征碼

隨著網(wǎng)絡(luò)應(yīng)用的日益增多和新的網(wǎng)絡(luò)技術(shù)的不斷出現(xiàn)，網(wǎng)絡(luò)流量的控制和管理面臨著新的挑戰(zhàn)。尤其是P2P技術(shù)的出現(xiàn)，給網(wǎng)絡(luò)路由器造成了極大的負(fù)擔(dān)，導(dǎo)致很多正常的網(wǎng)絡(luò)業(yè)務(wù)無法正常運(yùn)轉(zhuǎn)。由此，市場上出現(xiàn)了流量控制系統(tǒng)，在一定程度緩解了流量對帶寬造成的壓力。但是目前的流量控制系統(tǒng)對協(xié)議識別率普遍較低，存在很多誤識別現(xiàn)象，給管理員的管理工作帶來很多不便。為了使協(xié)議識別更加精確，策略的配置更加合理，將采用形式化B方法對系統(tǒng)進(jìn)行建模、精化，在FreeBSD下實(shí)現(xiàn)該系統(tǒng)。

一、形式化B方法與流量控制系統(tǒng)

1.形式化B方法概述。B方法是一種對軟件系統(tǒng)進(jìn)行描述、設(shè)計和編碼的方法。這種方法涵蓋了軟件開發(fā)的各個方面，通過一系列的精化步驟進(jìn)行設(shè)計，產(chǎn)生了層次性體系結(jié)構(gòu)及代碼。建立在Zermelo - Frankel 集合論的基礎(chǔ)上，能夠嚴(yán)格地進(jìn)行形式化規(guī)格說明的正確性證明。采用抽象機(jī)符號(Abstract Machine Notation，AMN)對軟件的規(guī)格說明進(jìn)行類型檢測、動態(tài)驗(yàn)證、數(shù)學(xué)證明等確保設(shè)計過程的正確，具有精確性、無二義性、一致性、能進(jìn)行推理等特點(diǎn)。AMN 中結(jié)構(gòu)化的機(jī)制增強(qiáng)了信息隱藏和數(shù)據(jù)封裝，嚴(yán)密的部件接口控制確保了大型開發(fā)中各個部件的獨(dú)立開發(fā)。

2.流量控制系統(tǒng)概述。流量控制系統(tǒng)一般部署在內(nèi)網(wǎng)網(wǎng)關(guān)和路由器之間，對進(jìn)出口的流量進(jìn)行控制。網(wǎng)絡(luò)流量控制模型一般包括流量分類器、隊(duì)列管理器、流量整形器和流量監(jiān)測器等幾個部分。數(shù)據(jù)包首先經(jīng)過流量分類器，根據(jù)數(shù)據(jù)包的特征對該流量進(jìn)行特征碼識別，接著對識別后的數(shù)據(jù)包進(jìn)行分類匯總，再按照事先配置好的策略、優(yōu)先級將數(shù)據(jù)包發(fā)送至隊(duì)列管理器，如果該數(shù)據(jù)包是被禁用協(xié)議，則直接將該包丟棄。

在整個流量控制系統(tǒng)中，流量分類器起著最關(guān)鍵的作用，它是后續(xù)模塊的基礎(chǔ);隊(duì)列管理器收到不同的數(shù)據(jù)包后，通過不同的隊(duì)列調(diào)度算法，分配相應(yīng)的通道帶寬，并對關(guān)鍵業(yè)務(wù)分配保證帶寬，保障其網(wǎng)絡(luò)業(yè)務(wù)正常進(jìn)行;流量整形是調(diào)整數(shù)據(jù)傳輸?shù)钠骄俾剩菙?shù)據(jù)按照傳輸模式規(guī)定的速率進(jìn)行傳輸，盡量避免突發(fā)性通信量導(dǎo)致的擁塞問題，主要采用的算法有令牌桶算法;流量檢測器能夠?qū)?shù)據(jù)包的識別、數(shù)據(jù)包的傳輸進(jìn)行監(jiān)測分析，實(shí)時生成圖表和報表，供管理員參考。

二、開發(fā)過程

1.非形式的規(guī)范。一個數(shù)據(jù)包(Packet)包含源IP地址SourceIP、目的IP地址DestinationIP、源端口SourcePort、目的端口DestionationPort、協(xié)議Protocol、數(shù)據(jù)Data幾部分組成。其中協(xié)議分為TCP和UDP。當(dāng)數(shù)據(jù)包進(jìn)入分類器(Filter)后，分類器分別檢測數(shù)據(jù)包的幾個組成部分，接著設(shè)置(set)數(shù)據(jù)包的狀態(tài)(state)、數(shù)據(jù)通道(pipe)，根據(jù)檢測結(jié)果將其發(fā)送(send)至隊(duì)列管理器或直接丟棄(drop)。隊(duì)列管理器(Queue)首先創(chuàng)建(create)不同的通道帶寬(Pipe)，接著讀取數(shù)據(jù)包的數(shù)據(jù)通道的值，將其發(fā)送至相應(yīng)的通道。流量整形器(Flow)最后將數(shù)據(jù)發(fā)送至數(shù)據(jù)出口。流量檢測器(Monitor)用于生成圖表(graphic)(如圖所示):

2.規(guī)約開發(fā)。根據(jù)非形式規(guī)范分別對各個抽象機(jī)進(jìn)行規(guī)約描述。下面建立分類器Filter抽象機(jī)。Filter抽象機(jī)封裝了數(shù)據(jù)包的各種信息，集合PROTOCOL用來保存數(shù)據(jù)包可能的各種協(xié)議，集合STATE用來保存數(shù)據(jù)包的兩種狀態(tài)，集合PIPE用來保存數(shù)據(jù)包所要進(jìn)入的帶寬隊(duì)列(由策略預(yù)先制定)。Filter抽象機(jī)執(zhí)行2個操作，drop操作將符合丟棄策略(BlockIP、BlockPort、BlockData)的數(shù)據(jù)包直接丟棄掉，send操作將其他的數(shù)據(jù)包轉(zhuǎn)發(fā)至隊(duì)列管理器，并設(shè)置該數(shù)據(jù)包所要進(jìn)入的帶寬pipe，將數(shù)據(jù)包帶寬策略設(shè)置為100KB。

MACHINE

Filter(SourceIp，DestinationIp，SourcePort，DestionationPort，Protocol，Data)

SETS

PROTOCOL={tcp，udp}

STATE=[block，pass]

PIPE=[100KB，500KB，1MB]

CONSTANTS

SourceIp∈ipAddress∧

DestinationIp∈ipAddress∧

SourcePort∈NAT∧

SourcePort<65536∧

DestionationPort∈NAT∧

DestionationPort <65536∧

Protocol∈PROTOCOL∧

Data∈String

OPERATIONS

d?鄺drop=

PRE

state∈STATE

THEN

IF SourceIp∈BlockIP then

state:=block

ELSE IF DestinationIp∈BlockIP then

state:=block

ELSE IF SourcePort∈BlockPort then

state:=block

ELSE IF DestionationPort∈BlockPort then

state:=block

ELSE IF data∈BlockData then

state:=block

END

END;

s?鄺send=

PRE

state∈STATE∧

protocol∈PROTOCOL∧

pipe∈PIPE

THEN

IF SourceIp BlockIP∧Pipe=100KB then

state:=pass‖pipe:=100KB

ELSE IF DestinationIp BlockIP∧Pipe=100KB then

state:=pass‖pipe:=100KB

ELSE IF SourcePort BlockPort∧Pipe=100KB then

state:=pass‖pipe:=100KB

ELSE IF DestionationPort BlockPort∧Pipe=100KB then

state:=pass‖pipe:=100KB

ELSE IF data BlockData∧Pipe=100KB then

state:=pass‖pipe:=100KB

END

END

同樣可以依次構(gòu)造隊(duì)列管理器抽象機(jī)Queue、流量整形器抽象機(jī)Flow和流量檢測器抽象機(jī)Monitor。Queue抽象機(jī)根據(jù)數(shù)據(jù)包的pipe信息執(zhí)行create操作，建立相應(yīng)的帶寬通道，數(shù)據(jù)包通過后將其轉(zhuǎn)發(fā)。Flow抽象機(jī)create令牌桶操作，令牌桶滿后將多余數(shù)據(jù)包分組到令牌桶外的緩存區(qū)排隊(duì)。Monitor抽象機(jī)用來將數(shù)據(jù)包和其他3個機(jī)器搜集來的信息繪制成表格和圖表。

3.精化和系統(tǒng)實(shí)現(xiàn)。精化是一種用于將軟件系統(tǒng)的“抽象模型”(其規(guī)范)變換到另一種更具體一些的數(shù)學(xué)模型(實(shí)現(xiàn))的技術(shù)。主要目的是將抽象機(jī)經(jīng)過多次細(xì)化，逐步精化精化成一個可以執(zhí)行的程序，程序的正確性依賴于每一步精化的正確性，最終完成系統(tǒng)實(shí)現(xiàn)。在Filter抽象機(jī)中，可以對其進(jìn)一步精化，數(shù)據(jù)包的data部分我們可以建立特征庫，利用模式匹配算法將data中的特征值與特征庫進(jìn)行對比匹配，達(dá)到網(wǎng)絡(luò)應(yīng)用識別的目的。這一步實(shí)現(xiàn)后，接著可以加入時間的因素，有時無法通過一個簡單的數(shù)據(jù)包識別具體的網(wǎng)絡(luò)應(yīng)用，這就需要系統(tǒng)要有自動學(xué)習(xí)功能，通過一段時間的檢測分析，判斷出具體的網(wǎng)絡(luò)應(yīng)用。需要注意的是，在精化的過程中，每個抽象機(jī)都要重新進(jìn)行構(gòu)造，驗(yàn)證實(shí)現(xiàn)的正確性。具體的精化過程在文中不再進(jìn)行闡述。

提出了利用B方法實(shí)現(xiàn)網(wǎng)絡(luò)流量監(jiān)控系統(tǒng)的方法。利用B方法進(jìn)行系統(tǒng)建模，能夠充分發(fā)揮形式化方法的優(yōu)點(diǎn)，提高了數(shù)據(jù)包類型的識別率和系統(tǒng)的穩(wěn)定性。通過逐步精化和形式化證明，能夠驗(yàn)證系統(tǒng)的正確性，生成可執(zhí)行的系統(tǒng)程序，保證了系統(tǒng)的健壯性、穩(wěn)定性和可維護(hù)性。由于精化過程是個難點(diǎn)也是重點(diǎn)，是生成程序的前提，在該系統(tǒng)下的精化工作還將進(jìn)一步進(jìn)行下去。

參考文獻(xiàn)

[1]裘宗燕譯.B方法.北京:電子工業(yè)出版社，2004

[2]Tartanoglu F，Levy N，Issarny V，et al.Using the B Method for the Formalization of Coordinated Atomic Actions[J].Computing and Informatics，2004 (10):103～109

[3]林闖，單志廣，任豐原.計算機(jī)網(wǎng)絡(luò)的服務(wù)質(zhì)量(QoS).北京:清華大學(xué)出版社，2004:210～226

[4]陳展榮，徐娟，禹智濤.一種基于漏桶算法的模糊流量控制器的設(shè)計.廣東工業(yè)大學(xué)學(xué)報.2003(1):18～52