[發(fā)明專利]安卓系統(tǒng)環(huán)境下的網(wǎng)絡(luò)協(xié)議形式化描述工具

有效

• 申請(qǐng)?zhí)枺?/td>: 201410542038.1
• 申請(qǐng)日: 2014-10-15
• 公開（公告）號(hào): CN104360836A
• 公開（公告）日: 2015-02-18
• 發(fā)明（設(shè)計(jì)）人: 努爾布力;解男男;高程;阿洪阿吉;黃春虎;沙利瓦爾;楊志偉;王寧;王浩
• 申請(qǐng)（專利權(quán)）人: 新疆大學(xué)
• 主分類號(hào): G06F9/44
• 分類號(hào): G06F9/44;H04L29/06
• 代理公司: 吉林長(zhǎng)春新紀(jì)元專利代理有限責(zé)任公司 22100
• 代理人: 王怡敏

技術(shù)領(lǐng)域

????本發(fā)明涉及計(jì)算機(jī)網(wǎng)絡(luò)領(lǐng)域，特別涉及協(xié)議工程、安卓操作系統(tǒng)、網(wǎng)絡(luò)協(xié)議形式化描述方面，尤指一種安卓系統(tǒng)環(huán)境下的網(wǎng)絡(luò)協(xié)議形式化描述工具，是一種安卓系統(tǒng)環(huán)境下的網(wǎng)絡(luò)協(xié)議形式化描述和分析方法，以及以此為基礎(chǔ)的協(xié)議形式化分析工具。

背景技術(shù)

??安卓（Android）操作系統(tǒng)是Google于2007年11月宣布的基于Linux平臺(tái)的開源移動(dòng)操作系統(tǒng)，采用軟件堆層的架構(gòu)，主要分為三部分：底層以Linux內(nèi)核工作為基礎(chǔ)，由C語言開發(fā)，只提供基本功能；中間層包括函數(shù)庫(kù)和虛擬機(jī)，有C++開發(fā)；上層為各種應(yīng)用軟件，由各公司自行開發(fā)。系統(tǒng)結(jié)構(gòu)圖如附圖1。

Android系統(tǒng)的組件可以分為以下幾個(gè)部分：

（1）關(guān)鍵應(yīng)用程序（Applications）

Android系統(tǒng)與一系列核心應(yīng)用程序包一起發(fā)布，包括Email客戶端、SMS短消息程序，日歷，地圖，瀏覽器等。

（2）應(yīng)用程序框架

????開發(fā)人員可以完全訪問核心應(yīng)用程序所使用的API框架，這種設(shè)計(jì)簡(jiǎn)化了組件的重用，任何一個(gè)應(yīng)用程序都可以發(fā)布它的功能塊，并且其他的程序可以使用。其中包括視圖、內(nèi)容提供器、資源管理器等。

（3）系統(tǒng)運(yùn)行庫(kù)

????包括程序庫(kù)、和運(yùn)行庫(kù)，能夠被Android系統(tǒng)中的不同組件使用，提供了JAVA編程語言核心庫(kù)的大多數(shù)功能。

（4）Linux內(nèi)核

Android的核心系統(tǒng)依賴于Linux2.6內(nèi)核，如安全性、內(nèi)存管理、進(jìn)程管理、網(wǎng)絡(luò)協(xié)議和驅(qū)動(dòng)模型。Linux內(nèi)核也作為硬件和軟件棧之間的抽象層。

網(wǎng)絡(luò)協(xié)議形式化模型常用的主要包含三種：

（1）有限狀態(tài)機(jī)FSM

?????FSM是許多形式化方法的基礎(chǔ)，它可以實(shí)現(xiàn)與其他形式化方法的組合和轉(zhuǎn)換，并且易于自動(dòng)實(shí)現(xiàn)，因此在形式化描述中占有重要地位。基于FSM描述的協(xié)議驗(yàn)證可通過構(gòu)造可達(dá)樹來實(shí)現(xiàn)。FSM簡(jiǎn)單直觀，但描述能力有限，因此在通信協(xié)議的描述中，通常需要對(duì)其進(jìn)行擴(kuò)展和優(yōu)化。

（2）Petri網(wǎng)

Petri網(wǎng)是一種適合于并發(fā)、異步、分布式系統(tǒng)描述與分析的圖形數(shù)學(xué)工具，目前已經(jīng)成為網(wǎng)絡(luò)協(xié)議分析和設(shè)計(jì)的典型模型之一。Petri網(wǎng)在協(xié)議系統(tǒng)的描述和分析方面，有許多分析技術(shù)，例如可達(dá)性分析、不變量分析、構(gòu)造理論、形式語言理論等。為了在不同領(lǐng)域的應(yīng)用，從基本Petri網(wǎng)演化出許多擴(kuò)展的研究，包括謂詞/動(dòng)作Petri網(wǎng)，時(shí)間Petri網(wǎng)，隨機(jī)Petri網(wǎng)等。

（3）通信進(jìn)程演算CCS

????CCS是進(jìn)程代數(shù)的基礎(chǔ)，能夠嚴(yán)格的表述一個(gè)系統(tǒng)或進(jìn)程執(zhí)行時(shí)事件的時(shí)序性以及系統(tǒng)之間通信的特性。能以嚴(yán)密的代數(shù)演算方法驗(yàn)證協(xié)議的性質(zhì)，因此它也是計(jì)算機(jī)通信系統(tǒng)的基本理論模型之一。使用擴(kuò)展規(guī)則、限制規(guī)則以及其他運(yùn)算法則將包含組合算子的表達(dá)式擴(kuò)展為不包含組合算子的表達(dá)式，可以驗(yàn)證多個(gè)進(jìn)程組合而成的系統(tǒng)是否有活動(dòng)性和安全性。其優(yōu)點(diǎn)在于能夠精密的表達(dá)謝意的邏輯結(jié)構(gòu)和協(xié)議的時(shí)序性，但不能直觀的描述協(xié)議性質(zhì)。

網(wǎng)絡(luò)協(xié)議形式化描述語言通常是以嚴(yán)格的數(shù)學(xué)方法為基礎(chǔ)，并且有嚴(yán)格的語法和語義的定義，可以精確、完全的表達(dá)協(xié)議的功能、性能和行為，廣泛的應(yīng)用于協(xié)議的分析、驗(yàn)證、實(shí)現(xiàn)、測(cè)試等系統(tǒng)中。

網(wǎng)絡(luò)協(xié)議形式化描述語言通常分為公用部分和擴(kuò)展部分。公用部分定義了網(wǎng)絡(luò)協(xié)議的組成部分以及協(xié)議之間的關(guān)系，擴(kuò)展部分用于定義網(wǎng)絡(luò)協(xié)議的一些特殊的細(xì)節(jié)。在實(shí)際的描述系統(tǒng)中，系統(tǒng)所使用的公用部分都是相同的，而對(duì)于擴(kuò)展部分，各個(gè)系統(tǒng)有獨(dú)特的部分，因?yàn)楦鱾€(gè)系統(tǒng)所要描述的重點(diǎn)是不同的。

擴(kuò)展標(biāo)記語言（XML）是一種廣泛應(yīng)用的描述語言，源自于標(biāo)準(zhǔn)導(dǎo)引標(biāo)識(shí)語言SGML。XML是一種元標(biāo)記語言，可以根據(jù)不同需求定義不同的標(biāo)記語言，其語法主要包括元素、處理指令、注釋、屬性等。XML的特點(diǎn)主要體現(xiàn)在以下四點(diǎn)：（1）信息的描述與信息處理是分開的；（2）XML文檔具有自我描述能力；（3）XML具有很強(qiáng)的開放性和擴(kuò)展性；（4）XML文檔具有可驗(yàn)證性。

現(xiàn)有的針對(duì)安卓系統(tǒng)的研究，在協(xié)議形式化描述方面的研究較少，并且偏向于在理論層面。已有的系統(tǒng)或者工具，通常對(duì)網(wǎng)絡(luò)流量具有一定的限制，同時(shí)對(duì)所安裝的系統(tǒng)有較大的影響，因此限制了應(yīng)用。

發(fā)明內(nèi)容