一个机器检测的Micro-Dalvik虚拟机模型

来源：软件学报杂志2015年第2期北京时间：

作者：何炎祥,江南,李清安,张军,沈凡凡

单位：何炎祥，武汉大学 计算机学院, 湖北 武汉 430072 ;软件工程国家重点实验室武汉大学, 湖北 武汉 43007211,江南，武汉大学 计算机学院, 湖北 武汉 430072 ;湖北工业大学 计算机学院, 湖北 武汉 43007002,李清安，武汉大学 计算机学院, 湖北 武汉 430072 ;软件工程国家重点实验室武汉大学, 湖北 武汉 43007203,张军，武汉大学 计算机学院, 湖北 武汉 430072 ;东华理工大学 软件学院, 江西 南昌 33001304,沈凡凡，武汉大学 计算机学院, 湖北 武汉 43007205

摘要：给出了一个寄存器架构的虚拟机模型Micro-Dalvik,包括虚拟机指令集和虚拟机运行时状态的形式化,并以大步操作语义(big-step operational semantics)的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换.最后,以定理的形式描述了语义满足的性质,并得到证明.这个模型的指令集包括了大部分Dalvik虚拟机指令,为获得形式语义的清晰化,它在Dalvik VM指令集上进行了必要的抽象,对其实质没有改变,因而具有较大的实用性.该形式化模型通过了定理证明助手Isabelle/HOL的验证.

关键词：大步操作语义;形式化验证;定理证明;寄存器架构的虚拟机

基金资助：国家自然科学基金(91118003, 61170022)