【摘要】：給出了一個寄存器架構的虛擬機模型Micro-Dalvik,包括虛擬機指令集和虛擬機運行時狀態(tài)的形式化,并以大步操作語義(big-step operational semantics)的方式給出了指令單步執(zhí)行的狀態(tài)轉換以及定義在單步執(zhí)行上的自反傳遞閉包來表達虛擬機程序的運行時狀態(tài)轉換.最后,以定理的形式描述了語義滿足的性質,并得到證明.這個模型的指令集包括了大部分Dalvik虛擬機指令,為獲得形式語義的清晰化,它在Dalvik VM指令集上進行了必要的抽象,對其實質沒有改變,因而具有較大的實用性.該形式化模型通過了定理證明助手Isabelle/HOL的驗證.
[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.
【作者單位】： 武漢大學計算機學院;軟件工程國家重點實驗室(武漢大學);湖北工業(yè)大學計算機學院;東華理工大學軟件學院;
【基金】：國家自然科學基金(91118003,61170022)
【分類號】：TP302

【參考文獻】

相關期刊論文 前1條

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

【共引文獻】

相關期刊論文 前5條

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

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

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

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

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

相關會議論文 前1條

1 浦建開;孫娜;李衛(wèi)民;;基于ATLAS的航電系統(tǒng)通用自動化測試平臺設計[A];2014航空試驗測試技術學術交流會論文集[C];2014年

相關博士學位論文 前2條

1 陳瀟怡;數(shù)字權限表達語言的形式化模型及應用研究[D];武漢大學;2011年

2 黃滟鴻;面向實時嵌入式系統(tǒng)的中斷語義理論研究[D];華東師范大學;2014年

【二級參考文獻】

相關期刊論文 前6條

1 周明天;譚良;;可信計算及其進展[J];電子科技大學學報;2006年S1期

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

3 胡定磊,陳書明;低功耗編譯技術綜述[J];電子學報;2005年04期

4 唐遇星,鄧濵,周興銘;基于Trace-Cache的多級動態(tài)優(yōu)化框架設計[J];電子學報;2005年11期

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

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

【相似文獻】

相關期刊論文 前10條

1 陳雪梅;可視虛擬機關鍵技術研究[J];廣東科技;2005年08期

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

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

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

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

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

7 方向陽;;“虛擬機”在實驗教學中的應用探索[J];中國現(xiàn)代教育裝備;2006年11期

8 張廣敏;盤細平;涂杰;;Java虛擬機的面向對象性[J];計算機應用與軟件;2006年03期

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

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

相關會議論文 前10條

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

2 段翼真;王曉程;;可信安全虛擬機平臺的研究[A];第26次全國計算機安全學術交流會論文集[C];2011年

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

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

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

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

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

8 朱欣焰;蘇科華;毛繼國;龔健雅;;GIS符號虛擬機及實現(xiàn)方法研究[A];《測繪通報》測繪科學前沿技術論壇摘要集[C];2008年

9 于洋;陳曉東;俞承芳;李旦;;基于FPGA平臺的虛擬機建模與仿真[A];2007'儀表，自動化及先進集成技術大會論文集（一）[C];2007年

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

相關重要報紙文章 前10條

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

2 本報記者 郭濤;誰來填補虛擬機的安全漏洞[N];中國計算機報;2010年

3 本報記者 郭濤;VMware改變軟件銷售模式[N];中國計算機報;2010年

4 盆盆;真實的虛擬機[N];中國電腦教育報;2004年

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

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

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

8 Antone Gonsalves;Linux的虛擬化未來[N];中國計算機報;2007年

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

10 本報記者 郭濤;消除虛擬機備份的尷尬[N];中國計算機報;2012年

相關博士學位論文 前10條

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

2 劉海坤;虛擬機在線遷移性能優(yōu)化關鍵技術研究[D];華中科技大學;2012年

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

4 趙佳;虛擬機動態(tài)遷移的關鍵問題研究[D];吉林大學;2013年

5 鄧莉;基于虛擬機遷移的動態(tài)資源配置研究[D];華中科技大學;2013年

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

7 董玉雙;云平臺中虛擬機部署的關鍵問題研究[D];吉林大學;2014年

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

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

10 鄒瓊;Java虛擬機的自適應動態(tài)優(yōu)化[D];中國科學技術大學;2008年

相關碩士學位論文 前10條

1 鄧洋春;Java虛擬機關鍵機制研究與實踐[D];中南大學;2009年

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

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

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

5 吳曉丹;反病毒虛擬機關鍵技術研究[D];中國科學技術大學;2009年

6 趙彥琨;虛擬機管理平臺中的虛擬機代理服務機制研究[D];華中科技大學;2009年

7 袁e，

本文編號：2404631