基于LTL的軟件可信性指標分析方法研究.pdf

1、隨著計算機硬件技術(shù)和相關(guān)軟件技術(shù)日益成熟，軟件在人們?nèi)粘Ｉa(chǎn)生活中扮演著越來越重要的角色，并在工業(yè)、通訊業(yè)、醫(yī)療、軍事和航空航天等方面也得到了廣泛的應用。軟件系統(tǒng)在很多重要領域的應用使得這些領域?qū)浖到y(tǒng)的依賴不斷增加，這就使得計算機的應用環(huán)境變得更加復雜，比如軟件系統(tǒng)的規(guī)模變得越來越大，復雜度也變得越來越高。但是，計算機軟件不可避免的存在著各種漏洞，這將嚴重影響人們在生產(chǎn)和生活中的各項活動。因此，提高軟件的可信性和正確性，構(gòu)建高可信性

2、軟件已經(jīng)成為了近幾年軟件研究開發(fā)方向的熱點問題。運行時驗證作為一種輕量級的驗證技術(shù)可以作為傳統(tǒng)驗證技術(shù)的有效補充，這也使得運行時驗證技術(shù)在軟件可信性的領域中得到了廣泛的應用。它的主要特點是在軟件系統(tǒng)的運行過程中進行驗證，這也為實時糾正軟件錯誤奠定了基礎。
　　本文對軟件可信性運行時驗證理論進行了細致的分析研究，對運行時驗證的線性時序邏輯（Linear Temporal Logic，以下簡稱LTL）、自動機理論和運行時驗證工具等部分

3、進行了分析研究。針對運行時驗證監(jiān)控器的構(gòu)造，本文采用了運行時驗證工具面向方面編程中的JavaAOP技術(shù)和AspectJ技術(shù)實現(xiàn)了監(jiān)控器的設計，這種方法基于自動機轉(zhuǎn)化算法，利用自動機轉(zhuǎn)化方法將語義表達的屬性轉(zhuǎn)化為運行時驗證監(jiān)控器。其中，使用JavaAOP技術(shù)實現(xiàn)了對軟件系統(tǒng)的函數(shù)進行運行時的監(jiān)控，使用AspectJ技術(shù)實現(xiàn)了對軟件系統(tǒng)的變量進行運行時的監(jiān)控。并具體實現(xiàn)了監(jiān)控代碼插裝及事件、條件計算等問題。
　　本文實驗在Window