可信網路軟體的形式驗證

《可信網路軟體的形式驗證》是依託上海大學，由繆淮扣擔任項目負責人的面上項目。

基本介紹

• 中文名：可信網路軟體的形式驗證
• 項目類別：面上項目
• 項目負責人：繆淮扣
• 依託單位：上海大學

中文摘要

以網路軟體為研究對象，針對軟體可信性質中的正確性和安全性，研究確保軟體行為一致性和安全性驗證的理論和方法。主要包括：研究網路軟體的形式化行為建模與安全建模方法和自動抽取模型的方法、從整體功能層面和互動行為層面對網路軟體進行行為建模的方法、威脅驅動的網路軟體的形式化安全建模方法、Web套用的on-the-fly導航建模方法；研究自動生成一致性和安全行性質的方法、組合式的抽象精化驗證方法與技術；採用模型檢驗和定理證明結合的方法和技術驗證網路軟體的行為一致性和安全性；套用監控理論的可控制性原理對構件式系統進行安全性質的驗證。研究符號模型檢測、限界模型檢測、偏序規約模型檢測和組合模型檢測的理論。開發支持工具。該項研究對於提高網路軟體的可信性和質量有重大意義。研究成果可以廣泛套用到網路軟體的開發過程中。

結題摘要

以網路軟體為研究對象，針對軟體可信性質中的正確性和安全性，研究了確保軟體行為一致性和安全性驗證的理論和方法。提出了一種基於On-the-fly的Web導航行為建模方法和威脅驅動的Web套用On-The-Fly導航模型的驗證方法，採用威脅驅動方法設計和抽取用於性質檢驗的安全性質，對互動的Web套用建模並驗證給定的安全性質；基於模糊集的相關理論給出了服務流程可信性的運算法則、量化服務流程的可信性和相似服務流程的概念；提出了一種驗證帶有時間約束的Web服務的方法。引入了一種被稱為WS時間自動機的形式化技術，以捕獲Web服務套用的時間行為。在深入分析用戶和Web瀏覽器互動行為的基礎上，引入On-the-fly 策略並採用反例引導的抽象精化驗證方法對網路軟體的導航行為進行建模和驗證。為了對Web服務組合建模，提出一個基於馬爾可夫決策過程的Web服務機率行為模型。為了對Web服務組合檢驗，通過狀態商的機率等價關係進行抽象。基於反例引導的思想，疊代地進行抽象精化過程直到不再出現反例或反例被證實為真；用機率時間計算樹邏輯PTCTL公式描述錯誤偵測能力和錯誤容忍能力的性質，在機率模型檢驗器PRISM上執行驗證並輸出定量檢驗結果。將機率度量理念引入到經典的Petri網模型，找出Petri網系統與機率空間的對應關係，給出了其相應的變遷觸發規則和結構特徵。提出了一種非確定機率Petri網模型NPPN (nondeterministic probabilistic Petri net)系統，它可用於對帶有機率和非確定性的系統的行為進行定性和定量的建模和驗證。對形式規格說明語言Z與相應定理證明方法及其套用進行研究。此外，給出了基於模型驗證的測試用例生成方法。開發了支持工具。該項研究對於提高網路軟體的可信性和質量有重大意義。研究成果可以廣泛套用到網路軟體的開發過程中。課題組在本項目研究期間，積極開展了與國內外同行的學術交流，培養了多名博士和碩士研究生。