《基於APTL的開放系統模型檢測》是依託西安電子科技大學，由田聰擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於APTL的開放系統模型檢測
- 項目類別：青年科學基金項目
- 項目負責人：田聰
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
隨著國民經濟、國防建設和人民生活日益增長的需求以及網際網路技術的發展，開放環境下的軟體系統已成為重要的軟體系統。與封閉系統相比較，開放系統與環境不斷地互動，系統的行為隨環境的變化而變化，並且系統的行為影響著環境的變化。如何保障開放軟體系統的可信性，是可信軟體領域面臨的一個新的挑戰。本項目研究基於互動式投影時序邏輯APTL的開放系統模型檢測理論與方法。在現有的投影時序邏輯PTL的基礎上，通過將時序操作符擴展到Agent相關的時序操作符，建立基於並發博弈結構的APTL模型，包括該邏輯的語法、語義以及邏輯規則，並研究APTL的可判定性；建立基於並發博弈結構的自動機模型ACG，研究ACG的判空、求交等算法；研究基於ACG的APTL模型檢測算法，以及相應的狀態空間縮減技術，並開發相應的模型檢測支持工具。以分散式軟體系統為示範，研究基於APTL的模型檢測在開放系統中的套用。
結題摘要
本項目解決了命題投影時序邏輯（PPTL）的表達性問題，證明PPTL具有完全正則表達能力，並給出了PPTL的5個子集的刻畫；改進了PPTL的判定算法；建立了命題投影時序邏輯（PPTL）的公理系統；基於投影操作建立了柱面計算模型；提出了基於Agent的互動式投影時序邏輯APTL系統；定義了基於並發博弈結構的自動機模型；給出了基於APTL的開放軟體系統模型檢測算法；通過引入新的布爾變數將抽象模型精化問題歸結到多項式問題，從而避免了原有抽象精化中的NP完全問題，而且還可以得到更小的精化模型；提出了線性的虛假路徑檢測算法。在項目的資助下，課題組共發表論文48篇，其中國際期刊論文9篇（SCI收錄），英文專著章節1篇，重要國際會議論文28篇，國內重要期刊論文11篇，申請專利22項，獲軟體著作權5項。組織國際會議TASE 2011，合辦國際研討會WSFOL 2012，參加國際會議/研討會10餘次。
