[發(fā)明專利]基于擴(kuò)展UML的Web應(yīng)用形式化建模及驗(yàn)證方法

在審

• 申請?zhí)枺?/td>: 201810609329.6
• 申請日: 2018-06-13
• 公開（公告）號(hào): CN108830085A
• 公開（公告）日: 2018-11-16
• 發(fā)明（設(shè)計(jì)）人: 楊星星;李曉紅;侯慶志
• 申請（專利權(quán)）人: 天津大學(xué)
• 主分類號(hào): G06F21/57
• 分類號(hào): G06F21/57
• 代理公司: 天津市北洋有限責(zé)任專利代理事務(wù)所 12201
• 代理人: 李素蘭

本發(fā)明公開了一種基于擴(kuò)展UML的Web應(yīng)用形式化建模及驗(yàn)證方法，步驟(1)、提取所要設(shè)計(jì)的軟件系統(tǒng)的功能性需求，進(jìn)行需求分析；步驟(2)、進(jìn)行UML建模；步驟(3)、使用XML表示上述的UML2.3模型；步驟(4)、生成形式化描述；步驟(5)、進(jìn)行安全屬性驗(yàn)證。本發(fā)明提供了由UML2.3模型到形式化語言進(jìn)行自動(dòng)轉(zhuǎn)換的可行方法；對(duì)UML2.3中類圖、時(shí)序圖、狀態(tài)圖進(jìn)行擴(kuò)展，實(shí)現(xiàn)Web應(yīng)用中協(xié)議的驗(yàn)證，以及實(shí)現(xiàn)UML模型到pi演算形式化語言的自動(dòng)轉(zhuǎn)換，極大的降低直接對(duì)協(xié)議進(jìn)行形式化建模的難度；所用的形式化建模驗(yàn)證工具，并精化形式化驗(yàn)證模型；通過對(duì)驗(yàn)證結(jié)果的展示和攻擊路徑的分析，檢測到形式化模型的漏洞，有助于快速精化模型，高效地進(jìn)行缺陷檢測。

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

本專利涉及軟件需求分析形式化技術(shù)領(lǐng)域，特別是涉及結(jié)合安全屬性形式化分析與 驗(yàn)證領(lǐng)域的一種Web應(yīng)用形式化建模及驗(yàn)證方法。

背景技術(shù)

隨著軟件工程規(guī)模不斷擴(kuò)大，軟件的復(fù)雜性不斷增加，軟件系統(tǒng)更容易出現(xiàn)錯(cuò)誤和 紕漏。此外，在整個(gè)軟件生命周期中，修復(fù)系統(tǒng)漏洞的時(shí)間越滯后，其成本就越高昂。 因此，在軟件系統(tǒng)早期設(shè)計(jì)和建模階段就以軟件開發(fā)方法與形式化方法相結(jié)合的方式進(jìn) 行漏洞分析和缺陷檢測、確保系統(tǒng)的可靠性，對(duì)提升軟件質(zhì)量具有重要的意義。

目前主要通過對(duì)軟件需求的分析來實(shí)現(xiàn)對(duì)形式化方法進(jìn)行建模。常用的形式化語言 有Z語言、B語言、CSP以及pi演算等。用于對(duì)安全需求工程建模的形式化和半形式 化常見方法有：Z語言、UML等。UML的發(fā)展主要基于面向?qū)ο蟮姆椒ㄔO(shè)計(jì)(OOAD)， 它結(jié)合并進(jìn)一步發(fā)展了Booch的對(duì)象集合方法、JamesRumbaugh提出的對(duì)象建模技術(shù) OMT以及Jacobson中對(duì)用例的定義和表示。UML規(guī)范中支持多種視圖的建模，由于其 易用性和用戶友好性，UML在工程行業(yè)迅速發(fā)展，并在事實(shí)上，已經(jīng)成為了可視化建 模語言中的工業(yè)標(biāo)準(zhǔn)之一。

目前，通過形式化方法對(duì)安全協(xié)議進(jìn)行建模及驗(yàn)證，可以及時(shí)在設(shè)計(jì)階段找出協(xié)議 漏洞，保證了軟件工程的Web應(yīng)用中從設(shè)計(jì)到實(shí)現(xiàn)中的質(zhì)量問題。形式化方法具有嚴(yán) 謹(jǐn)性和可驗(yàn)證的特點(diǎn)，適用于對(duì)安全攸關(guān)的系統(tǒng)和協(xié)議進(jìn)行驗(yàn)證。另一方面，由于形式 化方法比較抽象，基于嚴(yán)格的數(shù)學(xué)理論和推導(dǎo)，對(duì)于軟件工程師及開發(fā)者而言，有相對(duì) 較高的應(yīng)用門檻，因此將形式化方法與常用的工程化建模方法結(jié)合，并進(jìn)行建模和轉(zhuǎn)換 是目前行之有效的一種方法。

然而，本發(fā)明針對(duì)上述現(xiàn)狀，通過研究分析發(fā)現(xiàn)雖然結(jié)合UML及形式化的方法可以降低建模難度，并為系統(tǒng)提供形式化的語義和驗(yàn)證，但現(xiàn)有的方法依然存在很多不足 之處：1)缺少Web應(yīng)用相關(guān)的協(xié)議的特點(diǎn)，只能針對(duì)部分安全協(xié)議進(jìn)行建模，沒有針 對(duì)相應(yīng)的領(lǐng)域建模提出系統(tǒng)的框架；2)通常使用一種或兩種視圖對(duì)系統(tǒng)進(jìn)行建模，由 于視圖選取的局限性，在驗(yàn)證協(xié)議時(shí)，會(huì)出現(xiàn)狀態(tài)爆炸的情況，同時(shí)使協(xié)議的轉(zhuǎn)換過程 變得十分復(fù)雜。

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

針對(duì)現(xiàn)有技術(shù)存在的上述問題，本發(fā)明提出了一種于擴(kuò)展UML的Web應(yīng)用形式化建模及驗(yàn)證方法，通過對(duì)UML2.3進(jìn)行擴(kuò)展建模，將UML方法和形式化方法的優(yōu)勢相 結(jié)合，并針對(duì)系統(tǒng)特點(diǎn)提出了輕量形式化框架，將系統(tǒng)模型的自動(dòng)轉(zhuǎn)換為形式化模型， 并進(jìn)行安全屬性驗(yàn)證。

本發(fā)明提出了一種基于擴(kuò)展UML的Web應(yīng)用形式化建模及驗(yàn)證方法，該方法包括以下流程：

步驟1、提取所要設(shè)計(jì)的軟件系統(tǒng)的功能性需求，進(jìn)行需求分析，

步驟2、進(jìn)行UML建模，通過自然語言描述需求以實(shí)現(xiàn)建模；或者，對(duì)Web應(yīng)用 獨(dú)有的特征進(jìn)行抽取，實(shí)現(xiàn)對(duì)軟件系統(tǒng)的建模，其中：例圖的建模表示軟件系統(tǒng)中關(guān)鍵 角色的相應(yīng)行為，而類圖的建模表示軟件系統(tǒng)中每個(gè)主要功能及系統(tǒng)中類之間的關(guān)系； 通過對(duì)UML2.3模型視圖進(jìn)行擴(kuò)展，進(jìn)行詳細(xì)建模，從而為自動(dòng)化轉(zhuǎn)換做出準(zhǔn)備，具體 包括：擴(kuò)展的類圖用于表示軟件系統(tǒng)的類型和靜態(tài)行為，擴(kuò)展的時(shí)序圖適用于對(duì)軟件系 統(tǒng)間消息傳遞進(jìn)行建模，而擴(kuò)展的狀態(tài)圖對(duì)軟件系統(tǒng)中行為對(duì)狀態(tài)的遷移進(jìn)行表示；