【摘要】：動(dòng)態(tài)下推網(wǎng)絡(luò)(DPN,Dynamic Pushdown Networks)由一組能刻畫動(dòng)態(tài)創(chuàng)建線程的動(dòng)態(tài)下推系統(tǒng)(DPDS,Dynamic Push Down Systems)組成.本文首先將描述連續(xù)時(shí)間的實(shí)時(shí)時(shí)鐘引入DPN,提出了時(shí)間動(dòng)態(tài)下推網(wǎng)絡(luò)(TDPN,Timed Dynamic Pushdown Networks),能對(duì)動(dòng)態(tài)創(chuàng)建線程的實(shí)時(shí)并發(fā)遞歸系統(tǒng)建模;然后基于時(shí)鐘關(guān)鍵點(diǎn)的時(shí)鐘等價(jià)優(yōu)化方法,并采用on-the-fly技術(shù),僅關(guān)心棧頂及下一層的域狀態(tài)轉(zhuǎn)換,動(dòng)態(tài)的將連續(xù)時(shí)間模型TDPN轉(zhuǎn)換為時(shí)間域表示的離散模型DPN,同時(shí)給出TDPN到DPN的轉(zhuǎn)換算法;最后證明在TDPN中的可達(dá)狀態(tài)當(dāng)且僅當(dāng)其轉(zhuǎn)換狀態(tài)在DPN中可達(dá),從而可解決帶動(dòng)態(tài)線程創(chuàng)建的實(shí)時(shí)并發(fā)系統(tǒng)的可達(dá)性分析.
[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é)廣西可信軟件重點(diǎn)實(shí)驗(yàn)室;
【基金】：國家自然科學(xué)基金(No.61262008,No.61562015,No.61572146,No.U1501252) 廣西高等學(xué)校高水平創(chuàng)新團(tuán)隊(duì) 卓越學(xué)者計(jì)劃 廣西自然科學(xué)基金(No.2014GXNSFAA118365,No.2015GXNSFDA139038) 廣西可信軟件重點(diǎn)實(shí)驗(yàn)室重點(diǎn)基金 桂林電子科技大學(xué)創(chuàng)新團(tuán)隊(duì)
【分類號(hào)】：TP301.1;TP311.1

【相似文獻(xiàn)】

相關(guān)期刊論文 前5條

1 繆力;張大方;;通信下推系統(tǒng)的一種有界可達(dá)算法[J];計(jì)算機(jī)工程與應(yīng)用;2008年24期

2 孫聰;唐禮勇;陳鐘;;基于下推系統(tǒng)可達(dá)性分析的輸出信道信息流檢測[J];計(jì)算機(jī)科學(xué);2011年07期

3 孫聰;唐禮勇;陳鐘;;基于下推系統(tǒng)可達(dá)性分析的程序機(jī)密消去機(jī)制[J];軟件學(xué)報(bào);2012年08期

4 劉耀東;為BROWSE配置下推按鈕[J];電腦編程技巧與維護(hù);1995年09期

5 孫聰;唐禮勇;陳鐘;馬建峰;;基于加權(quán)下推系統(tǒng)優(yōu)化可達(dá)性分析的Java安全信息流研究[J];計(jì)算機(jī)研究與發(fā)展;2012年05期

相關(guān)碩士學(xué)位論文 前1條

1 靳陽;良結(jié)構(gòu)下推系統(tǒng)的表達(dá)能力[D];上海交通大學(xué);2015年

，

本文編號(hào)：2264363