基于UML行為模型的軟件漏洞檢測形式方法研究.pdf

1、隨著計算機應(yīng)用的不斷發(fā)展,人們對軟件的高可靠性要求越來越高。形式化方法是基于數(shù)學(xué)和邏輯語言的精確性規(guī)格、驗證,保證軟件高可靠性的重要方法。模型檢測是一種形式化的驗證技術(shù),對該理論的研究和應(yīng)用成為國內(nèi)外近幾年的熱點問題。在計算機硬件、安全協(xié)議驗證等領(lǐng)域,模型檢測技術(shù)已經(jīng)取得了豐碩的成果。
　　 為了實現(xiàn)軟件的高可靠性,首先要對影響軟件可靠性的軟件漏洞進行學(xué)習(xí)和研究。論文不僅介紹了軟件漏洞的分類而且對幾種具體的漏洞進行了分析和定義。

2、時序邏輯語言是模型檢測的基礎(chǔ),為了掌握模型檢測技術(shù),對線性時序邏輯語言LTL進行了詳細的描述,使用LTL對分析得到的漏洞定義進行了描述,從而得到了LTL公式。并且詳細地介紹了模型檢測工具SPIN。通過對SET購買過程協(xié)議使用SPIN進行驗證,更深入的了解了該模型檢測工具的建模語言promela以及屬性定義語言LTL。
　　 模型檢測技術(shù)應(yīng)用在軟件漏洞檢測領(lǐng)域主要包括對需求分析和設(shè)計階段的軟件模型進行模型檢測和對目標(biāo)代碼的模型檢測

3、。本課題選擇了對軟件開發(fā)初期階段的設(shè)計模型進行形式化驗證,可以及早的規(guī)避軟件邏輯漏洞和安全漏洞,大大減少軟件開發(fā)成本,縮短軟件開發(fā)周期。并且對軟件設(shè)計模型的形式化驗證基于UML行為模型。UML建模是目前軟件開發(fā)中最主要的可視化建模方法,而模型檢測等形式化方法在建模過程中存在可視化困難,因此,將兩種方法結(jié)合進行軟件漏洞的檢測,可以有效地減少形式化建模方面的難題。
　　 本課題主要研究在軟件開發(fā)初期,對UML行為模型進行模型檢測。首