安全協(xié)議UML模型的SPIN分析.pdf

1、UML是一種通用的面向?qū)ο蠼ＵZ言，具有很強(qiáng)的描述能力和良好的擴(kuò)展機(jī)制，但UML缺少精確的語義，不能對(duì)UML模型作進(jìn)一步分析和驗(yàn)證。形式化方法具有精確的數(shù)學(xué)語義和自動(dòng)化驗(yàn)證工具的支持，可以對(duì)軟件規(guī)范進(jìn)行嚴(yán)格的分析和驗(yàn)證，但形式化方法存在難以設(shè)計(jì)大型軟件，直接用形式化規(guī)范對(duì)系統(tǒng)建模難度大等缺點(diǎn)。為保證安全協(xié)議設(shè)計(jì)的正確性，在早期的時(shí)候發(fā)現(xiàn)可能存在的錯(cuò)誤，對(duì)協(xié)議的UML模型進(jìn)行形式化驗(yàn)證很有必要。 本文試圖結(jié)合面向?qū)ο蠛托问交椒ǖ?/p>

2、優(yōu)點(diǎn)，提出了一種將安全協(xié)議的UML模型轉(zhuǎn)換成PROMELA規(guī)范的方法。首先選取UML的包括類圖、序列圖和狀態(tài)圖的核心子集來建模安全協(xié)議，然后定義了該UML子集到PROMELA語言的轉(zhuǎn)換規(guī)則，根據(jù)規(guī)則將它自動(dòng)轉(zhuǎn)換成PROMELA規(guī)范，再調(diào)用模型檢測器SPIN進(jìn)行分析。該方法避免了直接使用形式化的PROMELA語言對(duì)協(xié)議建模，降低了分析協(xié)議的難度和出錯(cuò)的可能，具有較高的分析可靠性和效率；該原型系統(tǒng)經(jīng)進(jìn)一步完善后，可作為以網(wǎng)絡(luò)認(rèn)證協(xié)議為核心的