基于時間動態(tài)下推網(wǎng)絡(luò)可達性分析
發(fā)布時間：2018-10-11 13:35
【摘要】：動態(tài)下推網(wǎng)絡(luò)(DPN,Dynamic Pushdown Networks)由一組能刻畫動態(tài)創(chuàng)建線程的動態(tài)下推系統(tǒng)(DPDS,Dynamic Push Down Systems)組成.本文首先將描述連續(xù)時間的實時時鐘引入DPN,提出了時間動態(tài)下推網(wǎng)絡(luò)(TDPN,Timed Dynamic Pushdown Networks),能對動態(tài)創(chuàng)建線程的實時并發(fā)遞歸系統(tǒng)建模;然后基于時鐘關(guān)鍵點的時鐘等價優(yōu)化方法,并采用on-the-fly技術(shù),僅關(guān)心棧頂及下一層的域狀態(tài)轉(zhuǎn)換,動態(tài)的將連續(xù)時間模型TDPN轉(zhuǎn)換為時間域表示的離散模型DPN,同時給出TDPN到DPN的轉(zhuǎn)換算法;最后證明在TDPN中的可達狀態(tài)當且僅當其轉(zhuǎn)換狀態(tài)在DPN中可達,從而可解決帶動態(tài)線程創(chuàng)建的實時并發(fā)系統(tǒng)的可達性分析.
[Abstract]:Dynamic pushdown network (DPN,Dynamic Pushdown Networks) consists of a set of dynamic push systems (DPDS,Dynamic Push Down Systems) that can depict dynamically created threads. In this paper, a real-time clock describing continuous time is introduced into DPN,. A time-dynamic pushdown network (TDPN,Timed Dynamic Pushdown Networks),) is proposed to model the real-time concurrent recursive system with dynamically created threads, and then the clock equivalence optimization method based on the key points of the clock is proposed. Using on-the-fly technology, we only care about the domain state transition between the top of stack and the next layer, and dynamically convert the continuous time model (TDPN) into the discrete model (DPN,) expressed in time domain. At the same time, we give the transform algorithm from TDPN to DPN. Finally, the reachable state in TDPN is proved if and only if the transition state is reachable in DPN, thus solving the reachability analysis of real-time concurrent systems created with dynamic threads.
【作者單位】： 桂林電子科技大學(xué)廣西可信軟件重點實驗室;
【基金】：國家自然科學(xué)基金(No.61262008,No.61562015,No.61572146,No.U1501252) 廣西高等學(xué)校高水平創(chuàng)新團隊 卓越學(xué)者計劃 廣西自然科學(xué)基金(No.2014GXNSFAA118365,No.2015GXNSFDA139038) 廣西可信軟件重點實驗室重點基金 桂林電子科技大學(xué)創(chuàng)新團隊
【分類號】：TP301.1;TP311.1
本文編號：2264363
[Abstract]:Dynamic pushdown network (DPN,Dynamic Pushdown Networks) consists of a set of dynamic push systems (DPDS,Dynamic Push Down Systems) that can depict dynamically created threads. In this paper, a real-time clock describing continuous time is introduced into DPN,. A time-dynamic pushdown network (TDPN,Timed Dynamic Pushdown Networks),) is proposed to model the real-time concurrent recursive system with dynamically created threads, and then the clock equivalence optimization method based on the key points of the clock is proposed. Using on-the-fly technology, we only care about the domain state transition between the top of stack and the next layer, and dynamically convert the continuous time model (TDPN) into the discrete model (DPN,) expressed in time domain. At the same time, we give the transform algorithm from TDPN to DPN. Finally, the reachable state in TDPN is proved if and only if the transition state is reachable in DPN, thus solving the reachability analysis of real-time concurrent systems created with dynamic threads.
【作者單位】： 桂林電子科技大學(xué)廣西可信軟件重點實驗室;
【基金】：國家自然科學(xué)基金(No.61262008,No.61562015,No.61572146,No.U1501252) 廣西高等學(xué)校高水平創(chuàng)新團隊 卓越學(xué)者計劃 廣西自然科學(xué)基金(No.2014GXNSFAA118365,No.2015GXNSFDA139038) 廣西可信軟件重點實驗室重點基金 桂林電子科技大學(xué)創(chuàng)新團隊
【分類號】：TP301.1;TP311.1
【相似文獻】
相關(guān)期刊論文 前5條
1 繆力;張大方;;通信下推系統(tǒng)的一種有界可達算法[J];計算機工程與應(yīng)用;2008年24期
2 孫聰;唐禮勇;陳鐘;;基于下推系統(tǒng)可達性分析的輸出信道信息流檢測[J];計算機科學(xué);2011年07期
3 孫聰;唐禮勇;陳鐘;;基于下推系統(tǒng)可達性分析的程序機密消去機制[J];軟件學(xué)報;2012年08期
4 劉耀東;為BROWSE配置下推按鈕[J];電腦編程技巧與維護;1995年09期
5 孫聰;唐禮勇;陳鐘;馬建峰;;基于加權(quán)下推系統(tǒng)優(yōu)化可達性分析的Java安全信息流研究[J];計算機研究與發(fā)展;2012年05期
相關(guān)碩士學(xué)位論文 前1條
1 靳陽;良結(jié)構(gòu)下推系統(tǒng)的表達能力[D];上海交通大學(xué);2015年
，本文編號：2264363
本文鏈接：http://www.sikaile.net/kejilunwen/ruanjiangongchenglunwen/2264363.html
最近更新
教材專著
