1、由設(shè)計瑕疵引起的安全問題占據(jù)了系統(tǒng)開發(fā)過程中出現(xiàn)的安全性問題的50％，因此，無論在多么堅實的軟件安全程序中，對于系統(tǒng)體系結(jié)構(gòu)的風(fēng)險分析都顯得十分重要。安全性風(fēng)險分析是一種將技術(shù)問題和數(shù)據(jù)考量等相聯(lián)系的自然方法，是在軟件系統(tǒng)開發(fā)生命周期的初期階段就需要完成的步驟。安全風(fēng)險分析的結(jié)果和風(fēng)險類別同時也驅(qū)動了軟件安全性需求分析和安全性測試。
　　 系統(tǒng)安全性需求分析與建模是將風(fēng)險分析的過程放在了軟件生命周期的早期需求層，這是進行軟件體系

2、結(jié)構(gòu)風(fēng)險分析的最佳選擇。現(xiàn)有的軟件安全分析與建模方法主要包括:創(chuàng)建安全對象及分析評估故障樹;在軟件生命周期的整個過程中跟蹤關(guān)鍵安全需求;在軟件質(zhì)量模型基礎(chǔ)上添加安全標(biāo)準(zhǔn)和度量等。而這些方法和模型與傳統(tǒng)的軟件設(shè)計模型存在一定差異。系統(tǒng)的安全模型往往需要進行嚴(yán)格的形式化分析與驗證，因此有必要使用更為嚴(yán)格的過程管理及形式化的設(shè)計與分析方法對軟件安全性進行驗證。
　　 使用Unified Modeling Language(UML)統(tǒng)一

3、建模語言來對軟件系統(tǒng)進行建模是現(xiàn)在最流行的建模方式，但是對于要求嚴(yán)格的系統(tǒng)安全模型，有必要對UML建立的模型進行形式化來分析其可行性。論文在自動機理論基礎(chǔ)上提出了描述UML視圖的形式化機制，并將其映射到模型語言Promela，從而實現(xiàn)對使用UML建立的軟件安全模型的形式化，使得由非形式化的UML語言建立的軟件安全模型能夠得到更清晰嚴(yán)格的描述。過程中使用線性時序邏輯語言LTL定義軟件安全屬性，描述直觀并具有良好的兼容性。最后以形式化后的模