基于LTL的軟件可信性指標(biāo)分析方法研究.pdf

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

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

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