[發明專利]時間多棧下推網絡的靜態轉換方法

有效

• 申請號: 201510581206.2
• 申請日: 2015-09-14
• 公開（公告）號: CN105260295B
• 公開（公告）日: 2018-09-25
• 發明（設計）人: 錢俊彥;甘鵬程;郭云川;趙嶺忠;古天龍
• 申請（專利權）人: 桂林電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F21/57
• 代理公司: 桂林市持衡專利商標事務所有限公司 45107
• 代理人: 陳躍琳

本發明公開一種時間多棧下推網絡的靜態轉換方法，首先，為了描述實時系統中并發遞歸機制，以及線程之間的交互，在MPDN的基礎上引入時鐘，提出TMPDN模型，并給出其語法及操作語義。其次，利用時鐘域等價的優化技術，通過靜態轉換方法，將連續時間的TMPDN模型轉換成離散的MPDN模型。本發明能夠實現同時實現實時并發系統的實時性和并發性的描述，并能為實時并發程序的形式化驗證提供保證。

技術領域

本發明屬于軟件安全性和可靠性研究領域，涉及實時并發程序的驗證方法，是一種實時并發程序抽象模型的靜態轉換技術，具體涉及一種時間多棧下推網絡的靜態轉換方法。

背景技術

隨著多核處理器技術日益發展，并發軟件已滲透到國民經濟和國防建設的各個領域，然而軟件上微小錯誤可能導致重大事故，甚至危及人身安全，諸如交通控制和航空航天等領域。如何提高軟件系統的可靠性和安全性已成為當前緊迫問題。對于一些安全攸關的實時系統來說，其安全性要求更高，需充分驗證軟件系統的某些關鍵性質，故對其形式化分析驗證顯得尤為重要。

諸多學者已致力于實時系統分析與驗證的研究，為了描述不同類型的實時系統，提出了時間自動機、時間下推自動機、時間遞歸狀態自動機、嵌套時間自動機等理論模型。具體而言，1994年Alur(Alur R,Dill D.A theory of timed automata.TheoreticalComputer Science,1994,126(2):183-235)在自動機的基礎上，引入描述連續時間的時鐘，提出了時間自動機，并采用時鐘等價技術實現模型檢驗時間自動機(Bengtsson J,WangY.Timed automata:Semantics,algorithms and tools//Proceedings of the 4thAdvanced Course on Petri Nets.Eichstaat.Germany,2004:87-124)。為了解決含有遞歸的實時系統建模，Abdulla(Abdulla P A,Atig M F,Stenamn J.Adding time to pushdownautomata//Proceedings of the 1st workshop on Quantities in FormalMethods.Paris,France,2012:1-16)提出時間下推自動機，通過時間離散化，轉換為下推自動機，然后對其進行分析，并在文獻(Abdulla P A,Atig M F,Stenamn J.Minimal costreachability problem in priced timed pushdown systems//Proceedings of the 6thInternational Conference on Language and Automata Theory andApplications.Tarragona,Spain,2012:58-69)中加入權值，求解最小時間花費的可達性問題，2014年Cai(Cai X,Ogawa M.Well-structured pushdown system:case of densetimed pushdown automata//Proceedings of the 12th International Symposium onFunctional and Logic Programming.Kanazawa,Japan,2014:336-352)給出了一個時間下推自動機的實例；Trivedi(Trivedi A,Wojtczak D.Recursive timed automata//Proceedings of the 8th International Symposium on Automated Technology forVerification and Analysis.Singapore,2010:306–324)和Benerecetti(Benerecetti M,Minopoli S,Peron A.Analysis of timed recursive state machines//Proceedings ofthe 17th International Symposium on Temporal Representation andReasoning.Paris,France,2010:61–68)提出了時間遞歸狀態自動機，通過相互調用來實現遞歸描述，調用過程中，時鐘通過值或者引用的方式傳遞的；2013年Li(Guoqiang L,Xiaojuan C,Mizuhito O,Shoji Y.Nested timed automata//Proceedings of the 11thInternational Conference on Formal Modeling and Analysis of TimedSystems.Buenos Aires,Argentina,2013:168-182)提出了嵌套時間自動機(NeTAs)，其整體是一個下推自動機，棧的每一層為時間自動機，利用嵌套的思想來解決實時系統中的遞歸問題。上述模型能描述實時系統的并發及遞歸問題，但是無法描述實時并發系統中線程間交互的情況。