一个机器检测的Micro-Dalvik虚拟机模型
[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.
【作者单位】： 武汉大学计算机学院;软件工程国家重点实验室(武汉大学);湖北工业大学计算机学院;东华理工大学软件学院;
【基金】：国家自然科学基金(91118003,61170022)
【分类号】：TP302
【参考文献】
相关期刊论文 前1条
1 徐超;何炎祥;吴伟;陈勇;刘健博;;基于模拟关系的编译优化实现正确性验证方法[J];电子学报;2012年11期
【共引文献】
相关期刊论文 前5条
1 徐超;何炎祥;吴伟;陈勇;刘健博;;基于模拟关系的编译优化实现正确性验证方法[J];电子学报;2012年11期
2 徐超;何炎祥;陈勇;刘健博;吴伟;李清安;;一种多核系统可靠性加强的任务调度方法[J];电子学报;2013年05期
3 张玲波;甘元科;石刚;王生原;董渊;张智慧;王沿海;;同步数据流语言时态消去的可信翻译[J];计算机工程与设计;2014年01期
4 石刚;王生原;董渊;嵇智源;甘元科;张玲波;张煜承;王蕾;杨斐;;同步数据流语言可信编译器的构造[J];软件学报;2014年02期
5 刘洋;甘元科;王生原;董渊;杨斐;石刚;闫鑫;;同步数据流语言高阶运算消去的可信翻译[J];软件学报;2015年02期
相关会议论文 前1条
1 浦建开;孙娜;李卫民;;基于ATLAS的航电系统通用自动化测试平台设计[A];2014航空试验测试技术学术交流会论文集[C];2014年
相关博士学位论文 前2条
1 陈潇怡;数字权限表达语言的形式化模型及应用研究[D];武汉大学;2011年
2 黄滟鸿;面向实时嵌入式系统的中断语义理论研究[D];华东师范大学;2014年
【二级参考文献】
相关期刊论文 前6条
1 周明天;谭良;;可信计算及其进展[J];电子科技大学学报;2006年S1期
2 刘刚;陈意云;张志天;;循环不变形状图的自动推断[J];电子技术;2011年08期
3 胡定磊,陈书明;低功耗编译技术综述[J];电子学报;2005年04期
4 唐遇星,邓濵,周兴铭;基于Trace-Cache的多级动态优化框架设计[J];电子学报;2005年11期
5 胡定磊;陈书明;王凤芹;刘春林;;基于互补谓词的编译优化[J];电子学报;2006年07期
6 聂久焘;程旭;王克义;;一种高效的完全值编号算法[J];电子学报;2010年02期
【相似文献】
相关期刊论文 前10条
1 陈雪梅;可视虚拟机关键技术研究[J];广东科技;2005年08期
2 李超,方潜生;Java虚拟机中类装载机制的原理分析与应用研究[J];安徽建筑工业学院学报(自然科学版);2005年05期
3 张幼真;;用虚拟机实现多系统操作[J];微电脑世界;2005年09期
4 刘晖;;系统问答[J];电脑迷;2005年05期
5 朱海华;陈自刚;;Java虚拟机性能及调优[J];电脑知识与技术;2005年36期
6 杨丽洁;;虚拟机控制流的途径[J];河北工业大学成人教育学院学报;2005年04期
7 方向阳;;“虚拟机”在实验教学中的应用探索[J];中国现代教育装备;2006年11期
8 张广敏;盘细平;涂杰;;Java虚拟机的面向对象性[J];计算机应用与软件;2006年03期
9 北乡达郎;南庭;;嵌入式Java虚拟机渗透到手机以外的领域[J];电子设计应用;2007年10期
10 欧阳星明;朱金银;;虚拟机的可定制生成及其动态优化[J];计算机工程与科学;2008年01期
相关会议论文 前10条
1 孟广平;;虚拟机漂移网络连接方法探讨[A];中国计量协会冶金分会2011年会论文集[C];2011年
2 段翼真;王晓程;;可信安全虚拟机平台的研究[A];第26次全国计算机安全学术交流会论文集[C];2011年
3 李明宇;张倩;吕品;;网络流量感知的虚拟机高可用动态部署研究[A];2014第二届中国指挥控制大会论文集（上）[C];2014年
4 林红;;Java虚拟机面向数字媒体的应用研究[A];计算机技术与应用进展——全国第17届计算机科学与技术应用（CACIS）学术会议论文集（上册）[C];2006年
5 杨旭;彭一明;刑承杰;李若淼;;基于VMware vSphere 5虚拟机的备份系统实现[A];中国高等教育学会教育信息化分会第十二次学术年会论文集[C];2014年
6 沈敏虎;查德平;刘百祥;赵泽宇;;虚拟机网络部署与管理研究[A];中国高等教育学会教育信息化分会第十次学术年会论文集[C];2010年
7 李英壮;廖培腾;孙梦;李先毅;;基于云计算的数据中心虚拟机管理平台的设计[A];中国高等教育学会教育信息化分会第十次学术年会论文集[C];2010年
8 朱欣焰;苏科华;毛继国;龚健雅;;GIS符号虚拟机及实现方法研究[A];《测绘通报》测绘科学前沿技术论坛摘要集[C];2008年
9 于洋;陈晓东;俞承芳;李旦;;基于FPGA平台的虚拟机建模与仿真[A];2007'仪表，自动化及先进集成技术大会论文集（一）[C];2007年
10 丁涛;郝沁汾;张冰;;内核虚拟机调度策略的研究与分析[A];'2010系统仿真技术及其应用学术会议论文集[C];2010年
相关重要报纸文章 前10条
1 宁家雨;虚拟机数据在哪个磁盘上？[N];网络世界;2009年
2 本报记者 郭涛;谁来填补虚拟机的安全漏洞[N];中国计算机报;2010年
3 本报记者 郭涛;VMware改变软件销售模式[N];中国计算机报;2010年
4 盆盆;真实的虚拟机[N];中国电脑教育报;2004年
5 ;利用工具解决虚拟机监测难题[N];网络世界;2007年
6 宋家雨;别拿虚拟机不当固定资产[N];网络世界;2008年
7 《网络世界》记者 柴莎莎;虚拟机通信可视性很关键[N];网络世界;2011年
8 Antone Gonsalves;Linux的虚拟化未来[N];中国计算机报;2007年
9 张承东;安全争议让虚拟化用户“心虚”[N];网络世界;2007年
10 本报记者 郭涛;消除虚拟机备份的尴尬[N];中国计算机报;2012年
相关博士学位论文 前10条
1 陈彬;分布环境下虚拟机按需部署关键技术研究[D];国防科学技术大学;2010年
2 刘海坤;虚拟机在线迁移性能优化关键技术研究[D];华中科技大学;2012年
3 刘谦;面向云计算的虚拟机系统安全研究[D];上海交通大学;2012年
4 赵佳;虚拟机动态迁移的关键问题研究[D];吉林大学;2013年
5 邓莉;基于虚拟机迁移的动态资源配置研究[D];华中科技大学;2013年
6 李丁丁;虚拟机本地存储写性能优化研究[D];华中科技大学;2013年
7 董玉双;云平台中虚拟机部署的关键问题研究[D];吉林大学;2014年
8 曹文治;虚拟机网络性能优化研究[D];华中科技大学;2013年
9 杜雨阳;虚拟机状态迁移和相变存储磨损均衡方法研究[D];清华大学;2011年
10 邹琼;Java虚拟机的自适应动态优化[D];中国科学技术大学;2008年
相关硕士学位论文 前10条
1 邓洋春;Java虚拟机关键机制研究与实践[D];中南大学;2009年
2 陆晓雯;虚拟机资源监测调整机制研究[D];华中科技大学;2008年
3 杨卫平;面向虚拟机的网络入侵检测系统[D];华中科技大学;2008年
4 张德;硬件虚拟机的域间通讯和性能模型研究[D];华中科技大学;2008年
5 吴晓丹;反病毒虚拟机关键技术研究[D];中国科学技术大学;2009年
6 赵彦琨;虚拟机管理平台中的虚拟机代理服务机制研究[D];华中科技大学;2009年
7 袁e，
本文编号：2404631
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/2404631.html
