本文關鍵詞：基于時間多棧下推網(wǎng)絡的實時系統(tǒng)驗證，，由筆耕文化傳播整理發(fā)布。

【摘要】：多棧下推網(wǎng)絡(MPDN)是利用多個棧來描述并發(fā)遞歸程序線程之間交互的一種下推系統(tǒng)模型.為了描述基于線程之間交互的實時并發(fā)遞歸程序,首先將描述連續(xù)時間的時鐘引入到MPDN,提出了時間多棧下推網(wǎng)絡(TMPDN),并給出了語法及其操作語義;其次利用基于時間關鍵點的時鐘等價優(yōu)化技術,縮減等價域狀態(tài)空間;然后通過靜態(tài)轉換方法,獲得所有的可達域狀態(tài)格局,將連續(xù)時間的TMPDN模型轉換成離散的MPDN模型.在此基礎上,基于on-the-fly技術,采用動態(tài)轉換方法,僅關心棧頂域狀態(tài)轉換,進一步縮減轉換后的狀態(tài)空間.同時證明了狀態(tài)q_F在TMPDN可達當且僅當其轉換狀態(tài)q′_F在MPDN可達,并給出了模型轉換算法;最后可采用現(xiàn)有模型檢驗工具驗證轉換后的MPDN.
【作者單位】： 桂林電子科技大學廣西可信軟件重點實驗室;中國科學院信息工程研究所;
【關鍵詞】： MPDN TMPDN 并發(fā)遞歸程序 時鐘等價 可達性
【基金】：國家自然科學基金(61262008,61562015,61572146,U1501252) 廣西自然科學基金(2012GXNSFAA053220,2014GXNSFAA118365,2015GXNSFDA139038) 廣西高等學校高水平創(chuàng)新團隊及卓越學者計劃 廣西可信軟件重點實驗室重點基金 桂林電子科技大學創(chuàng)新團隊資助~~
【分類號】：TP311.1;TP301.1
【正文快照】： 科學基金(2012GXNSFAA053220,2014GXNSFAA118365,2015GXNSFDA139038)、廣西高等學校高水平創(chuàng)新團隊及卓越學者計劃、廣西可信軟件重點實驗室重點基金、桂林電子科技大學創(chuàng)新團隊資助.錢俊彥,男,1973年生,博士,教授,中國計算機學會(CCF)高級會員,主要研究領域為軟件工程、模型

  本文關鍵詞：基于時間多棧下推網(wǎng)絡的實時系統(tǒng)驗證，由筆耕文化傳播整理發(fā)布。

本文編號：445009