發(fā)布時(shí)間：2019-01-08 12:58

【摘要】：給出了一個(gè)寄存器架構(gòu)的虛擬機(jī)模型Micro-Dalvik,包括虛擬機(jī)指令集和虛擬機(jī)運(yùn)行時(shí)狀態(tài)的形式化,并以大步操作語(yǔ)義(big-step operational semantics)的方式給出了指令單步執(zhí)行的狀態(tài)轉(zhuǎn)換以及定義在單步執(zhí)行上的自反傳遞閉包來(lái)表達(dá)虛擬機(jī)程序的運(yùn)行時(shí)狀態(tài)轉(zhuǎn)換.最后,以定理的形式描述了語(yǔ)義滿(mǎn)足的性質(zhì),并得到證明.這個(gè)模型的指令集包括了大部分Dalvik虛擬機(jī)指令,為獲得形式語(yǔ)義的清晰化,它在Dalvik VM指令集上進(jìn)行了必要的抽象,對(duì)其實(shí)質(zhì)沒(méi)有改變,因而具有較大的實(shí)用性.該形式化模型通過(guò)了定理證明助手Isabelle/HOL的驗(yàn)證.
[Abstract]:In this paper, a register architecture virtual machine model (Micro-Dalvik,) is presented, which includes virtual machine instruction set and virtual machine runtime state formalization. The state transformation of instruction step execution and the reflexive transitive closure defined on single step execution are given in the form of big-step operational semantics) to express the runtime state transformation of virtual machine program. Finally, the properties of semantic satisfaction are described in the form of theorems and proved. The instruction set of this model includes most of the instructions of Dalvik virtual machine. In order to get the clarity of formal semantics, the instruction set of this model is abstracted from the Dalvik VM instruction set, and its essence is not changed, so it has great practicability. The formal model is verified by theorem proving assistant Isabelle/HOL.
【作者單位】： 武漢大學(xué)計(jì)算機(jī)學(xué)院;軟件工程國(guó)家重點(diǎn)實(shí)驗(yàn)室(武漢大學(xué));湖北工業(yè)大學(xué)計(jì)算機(jī)學(xué)院;東華理工大學(xué)軟件學(xué)院;
【基金】：國(guó)家自然科學(xué)基金(91118003,61170022)
【分類(lèi)號(hào)】：TP302

【參考文獻(xiàn)】

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

1 徐超;何炎祥;吳偉;陳勇;劉健博;;基于模擬關(guān)系的編譯優(yōu)化實(shí)現(xiàn)正確性驗(yàn)證方法[J];電子學(xué)報(bào);2012年11期

【共引文獻(xiàn)】

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

1 徐超;何炎祥;吳偉;陳勇;劉健博;;基于模擬關(guān)系的編譯優(yōu)化實(shí)現(xiàn)正確性驗(yàn)證方法[J];電子學(xué)報(bào);2012年11期

2 徐超;何炎祥;陳勇;劉健博;吳偉;李清安;;一種多核系統(tǒng)可靠性加強(qiáng)的任務(wù)調(diào)度方法[J];電子學(xué)報(bào);2013年05期

3 張玲波;甘元科;石剛;王生原;董淵;張智慧;王沿海;;同步數(shù)據(jù)流語(yǔ)言時(shí)態(tài)消去的可信翻譯[J];計(jì)算機(jī)工程與設(shè)計(jì);2014年01期

4 石剛;王生原;董淵;嵇智源;甘元科;張玲波;張煜承;王蕾;楊斐;;同步數(shù)據(jù)流語(yǔ)言可信編譯器的構(gòu)造[J];軟件學(xué)報(bào);2014年02期

5 劉洋;甘元科;王生原;董淵;楊斐;石剛;閆鑫;;同步數(shù)據(jù)流語(yǔ)言高階運(yùn)算消去的可信翻譯[J];軟件學(xué)報(bào);2015年02期

相關(guān)會(huì)議論文 前1條

1 浦建開(kāi);孫娜;李衛(wèi)民;;基于A(yíng)TLAS的航電系統(tǒng)通用自動(dòng)化測(cè)試平臺(tái)設(shè)計(jì)[A];2014航空試驗(yàn)測(cè)試技術(shù)學(xué)術(shù)交流會(huì)論文集[C];2014年

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

1 陳瀟怡;數(shù)字權(quán)限表達(dá)語(yǔ)言的形式化模型及應(yīng)用研究[D];武漢大學(xué);2011年

2 黃滟鴻;面向?qū)崟r(shí)嵌入式系統(tǒng)的中斷語(yǔ)義理論研究[D];華東師范大學(xué);2014年

【二級(jí)參考文獻(xiàn)】

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

1 周明天;譚良;;可信計(jì)算及其進(jìn)展[J];電子科技大學(xué)學(xué)報(bào);2006年S1期

2 劉剛;陳意云;張志天;;循環(huán)不變形狀圖的自動(dòng)推斷[J];電子技術(shù);2011年08期

3 胡定磊,陳書(shū)明;低功耗編譯技術(shù)綜述[J];電子學(xué)報(bào);2005年04期

4 唐遇星,鄧濵,周興銘;基于Trace-Cache的多級(jí)動(dòng)態(tài)優(yōu)化框架設(shè)計(jì)[J];電子學(xué)報(bào);2005年11期

5 胡定磊;陳書(shū)明;王鳳芹;劉春林;;基于互補(bǔ)謂詞的編譯優(yōu)化[J];電子學(xué)報(bào);2006年07期

6 聶久燾;程旭;王克義;;一種高效的完全值編號(hào)算法[J];電子學(xué)報(bào);2010年02期

【相似文獻(xiàn)】

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

1 陳雪梅;可視虛擬機(jī)關(guān)鍵技術(shù)研究[J];廣東科技;2005年08期

2 李超,方潛生;Java虛擬機(jī)中類(lèi)裝載機(jī)制的原理分析與應(yīng)用研究[J];安徽建筑工業(yè)學(xué)院學(xué)報(bào)(自然科學(xué)版);2005年05期

3 張幼真;;用虛擬機(jī)實(shí)現(xiàn)多系統(tǒng)操作[J];微電腦世界;2005年09期

4 劉暉;;系統(tǒng)問(wèn)答[J];電腦迷;2005年05期

5 朱海華;陳自剛;;Java虛擬機(jī)性能及調(diào)優(yōu)[J];電腦知識(shí)與技術(shù);2005年36期

6 楊麗潔;;虛擬機(jī)控制流的途徑[J];河北工業(yè)大學(xué)成人教育學(xué)院學(xué)報(bào);2005年04期

7 方向陽(yáng);;“虛擬機(jī)”在實(shí)驗(yàn)教學(xué)中的應(yīng)用探索[J];中國(guó)現(xiàn)代教育裝備;2006年11期

8 張廣敏;盤(pán)細(xì)平;涂杰;;Java虛擬機(jī)的面向?qū)ο笮訹J];計(jì)算機(jī)應(yīng)用與軟件;2006年03期

9 北鄉(xiāng)達(dá)郎;南庭;;嵌入式Java虛擬機(jī)滲透到手機(jī)以外的領(lǐng)域[J];電子設(shè)計(jì)應(yīng)用;2007年10期

10 歐陽(yáng)星明;朱金銀;;虛擬機(jī)的可定制生成及其動(dòng)態(tài)優(yōu)化[J];計(jì)算機(jī)工程與科學(xué);2008年01期

相關(guān)會(huì)議論文 前10條

1 孟廣平;;虛擬機(jī)漂移網(wǎng)絡(luò)連接方法探討[A];中國(guó)計(jì)量協(xié)會(huì)冶金分會(huì)2011年會(huì)論文集[C];2011年

2 段翼真;王曉程;;可信安全虛擬機(jī)平臺(tái)的研究[A];第26次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2011年

3 李明宇;張倩;呂品;;網(wǎng)絡(luò)流量感知的虛擬機(jī)高可用動(dòng)態(tài)部署研究[A];2014第二屆中國(guó)指揮控制大會(huì)論文集（上）[C];2014年

4 林紅;;Java虛擬機(jī)面向數(shù)字媒體的應(yīng)用研究[A];計(jì)算機(jī)技術(shù)與應(yīng)用進(jìn)展——全國(guó)第17屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用（CACIS）學(xué)術(shù)會(huì)議論文集（上冊(cè)）[C];2006年

5 楊旭;彭一明;刑承杰;李若淼;;基于VMware vSphere 5虛擬機(jī)的備份系統(tǒng)實(shí)現(xiàn)[A];中國(guó)高等教育學(xué)會(huì)教育信息化分會(huì)第十二次學(xué)術(shù)年會(huì)論文集[C];2014年

6 沈敏虎;查德平;劉百祥;趙澤宇;;虛擬機(jī)網(wǎng)絡(luò)部署與管理研究[A];中國(guó)高等教育學(xué)會(huì)教育信息化分會(huì)第十次學(xué)術(shù)年會(huì)論文集[C];2010年

7 李英壯;廖培騰;孫夢(mèng);李先毅;;基于云計(jì)算的數(shù)據(jù)中心虛擬機(jī)管理平臺(tái)的設(shè)計(jì)[A];中國(guó)高等教育學(xué)會(huì)教育信息化分會(huì)第十次學(xué)術(shù)年會(huì)論文集[C];2010年

8 朱欣焰;蘇科華;毛繼國(guó);龔健雅;;GIS符號(hào)虛擬機(jī)及實(shí)現(xiàn)方法研究[A];《測(cè)繪通報(bào)》測(cè)繪科學(xué)前沿技術(shù)論壇摘要集[C];2008年

9 于洋;陳曉東;俞承芳;李旦;;基于FPGA平臺(tái)的虛擬機(jī)建模與仿真[A];2007'儀表，自動(dòng)化及先進(jìn)集成技術(shù)大會(huì)論文集（一）[C];2007年

10 丁濤;郝沁汾;張冰;;內(nèi)核虛擬機(jī)調(diào)度策略的研究與分析[A];'2010系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2010年

相關(guān)重要報(bào)紙文章 前10條

1 寧家雨;虛擬機(jī)數(shù)據(jù)在哪個(gè)磁盤(pán)上？[N];網(wǎng)絡(luò)世界;2009年

2 本報(bào)記者 郭濤;誰(shuí)來(lái)填補(bǔ)虛擬機(jī)的安全漏洞[N];中國(guó)計(jì)算機(jī)報(bào);2010年

3 本報(bào)記者 郭濤;VMware改變軟件銷(xiāo)售模式[N];中國(guó)計(jì)算機(jī)報(bào);2010年

4 盆盆;真實(shí)的虛擬機(jī)[N];中國(guó)電腦教育報(bào);2004年

5 ;利用工具解決虛擬機(jī)監(jiān)測(cè)難題[N];網(wǎng)絡(luò)世界;2007年

6 宋家雨;別拿虛擬機(jī)不當(dāng)固定資產(chǎn)[N];網(wǎng)絡(luò)世界;2008年

7 《網(wǎng)絡(luò)世界》記者 柴莎莎;虛擬機(jī)通信可視性很關(guān)鍵[N];網(wǎng)絡(luò)世界;2011年

8 Antone Gonsalves;Linux的虛擬化未來(lái)[N];中國(guó)計(jì)算機(jī)報(bào);2007年

9 張承東;安全爭(zhēng)議讓虛擬化用戶(hù)“心虛”[N];網(wǎng)絡(luò)世界;2007年

10 本報(bào)記者 郭濤;消除虛擬機(jī)備份的尷尬[N];中國(guó)計(jì)算機(jī)報(bào);2012年

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

1 陳彬;分布環(huán)境下虛擬機(jī)按需部署關(guān)鍵技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2010年

2 劉海坤;虛擬機(jī)在線(xiàn)遷移性能優(yōu)化關(guān)鍵技術(shù)研究[D];華中科技大學(xué);2012年

3 劉謙;面向云計(jì)算的虛擬機(jī)系統(tǒng)安全研究[D];上海交通大學(xué);2012年

4 趙佳;虛擬機(jī)動(dòng)態(tài)遷移的關(guān)鍵問(wèn)題研究[D];吉林大學(xué);2013年

5 鄧?yán)?基于虛擬機(jī)遷移的動(dòng)態(tài)資源配置研究[D];華中科技大學(xué);2013年

6 李丁丁;虛擬機(jī)本地存儲(chǔ)寫(xiě)性能優(yōu)化研究[D];華中科技大學(xué);2013年

7 董玉雙;云平臺(tái)中虛擬機(jī)部署的關(guān)鍵問(wèn)題研究[D];吉林大學(xué);2014年

8 曹文治;虛擬機(jī)網(wǎng)絡(luò)性能優(yōu)化研究[D];華中科技大學(xué);2013年

9 杜雨陽(yáng);虛擬機(jī)狀態(tài)遷移和相變存儲(chǔ)磨損均衡方法研究[D];清華大學(xué);2011年

10 鄒瓊;Java虛擬機(jī)的自適應(yīng)動(dòng)態(tài)優(yōu)化[D];中國(guó)科學(xué)技術(shù)大學(xué);2008年

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

1 鄧洋春;Java虛擬機(jī)關(guān)鍵機(jī)制研究與實(shí)踐[D];中南大學(xué);2009年

2 陸曉雯;虛擬機(jī)資源監(jiān)測(cè)調(diào)整機(jī)制研究[D];華中科技大學(xué);2008年

3 楊衛(wèi)平;面向虛擬機(jī)的網(wǎng)絡(luò)入侵檢測(cè)系統(tǒng)[D];華中科技大學(xué);2008年

4 張德;硬件虛擬機(jī)的域間通訊和性能模型研究[D];華中科技大學(xué);2008年

5 吳曉丹;反病毒虛擬機(jī)關(guān)鍵技術(shù)研究[D];中國(guó)科學(xué)技術(shù)大學(xué);2009年

6 趙彥琨;虛擬機(jī)管理平臺(tái)中的虛擬機(jī)代理服務(wù)機(jī)制研究[D];華中科技大學(xué);2009年

7 袁e，

本文編號(hào)：2404631