基于形式化方法的統(tǒng)一軟件模型及其應用.pdf

1、隨著計算機應用的不斷發(fā)展，在信息社會中發(fā)揮著至關(guān)重要的作用。但是軟件的生產(chǎn)現(xiàn)狀不能令人滿意，軟件安全事故、軟件質(zhì)量問題、軟件擴展問題已經(jīng)帶來了巨大的損失。國內(nèi)外專家及行業(yè)巨頭已經(jīng)將軟件的可信性作為軟件的一個重要屬性，然而，目前多數(shù)研究主要還是針對安全性。
　　 本文將軟件可信性做一個多維的評估指標，通過軟件工程方法論的角度，針對軟件的功能性、可靠性、安全性、可維護性、可擴展性等性質(zhì)進行了研究，主要工作包括：
　　 1)提

2、出了基于形式化語言Z規(guī)格和UML視圖的統(tǒng)一軟件模型，基于該模型，構(gòu)建了軟件可信工程方法，該方法將形式化方法融入傳統(tǒng)軟件工程，繼承了形式化模型可驗證的優(yōu)點，并一定程度降低了形式化模型在大型項目中較高的復雜度、和傳統(tǒng)軟件工程大量的人為不確定因素。
　　 2)基于課題組軟件安全缺陷知識庫，實現(xiàn)了統(tǒng)一軟件模型在設(shè)計階段的軟件安全缺陷形式化檢測，從而在缺陷引入的最早階段快速發(fā)現(xiàn)并給出具體緩和方案，避免了設(shè)計階段的軟件安全缺陷在軟件生命周期

3、后期非常高昂的緩和成本、降低了軟件安全性保障對安全專家個人經(jīng)驗和知識的依賴。
　　 3)設(shè)計了軟件可信工程支持平臺，從工具角度提高了軟件可信工程的可實施性，并引入了結(jié)合統(tǒng)一軟件模型的項目管理機制降低了工程管理所引入的開發(fā)不確定性。
　　 本文搭建了一個結(jié)合了形式化方法的軟件工程理論體系，實現(xiàn)了軟件設(shè)計的一致性、有效性、安全性驗證，集成了課題組其他工作如模型驅(qū)動的單元測試、可信性評估等，同時，為將來的研究工作提供了理論基礎(chǔ)