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

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

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

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