| 一个机器检测的Micro-Dalvik虚拟机模型 |
| |
| 引用本文： | 何炎祥,江南,李清安,张军,沈凡凡.一个机器检测的Micro-Dalvik虚拟机模型[J].软件学报,2015,26(2):364-379. |
| |
| 作者姓名： | 何炎祥 江南 李清安 张军 沈凡凡 |
| |
| 作者单位： | 武汉大学 计算机学院, 湖北 武汉 430072
;软件工程国家重点实验室武汉大学, 湖北 武汉 430072,武汉大学 计算机学院, 湖北 武汉 430072
;湖北工业大学 计算机学院, 湖北 武汉 430070,武汉大学 计算机学院, 湖北 武汉 430072
;软件工程国家重点实验室武汉大学, 湖北 武汉 430072,武汉大学 计算机学院, 湖北 武汉 430072
;东华理工大学 软件学院, 江西 南昌 330013,武汉大学 计算机学院, 湖北 武汉 430072 |
| |
| 基金项目： | 国家自然科学基金(91118003, 61170022) |
| |
| 摘 要： | 给出了一个寄存器架构的虚拟机模型Micro-Dalvik,包括虚拟机指令集和虚拟机运行时状态的形式化,并以大步操作语义(big-step operational semantics)的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换.最后,以定理的形式描述了语义满足的性质,并得到证明.这个模型的指令集包括了大部分Dalvik虚拟机指令,为获得形式语义的清晰化,它在Dalvik VM指令集上进行了必要的抽象,对其实质没有改变,因而具有较大的实用性.该形式化模型通过了定理证明助手Isabelle/HOL的验证.
|
| 关 键 词： | 大步操作语义 形式化验证 定理证明 寄存器架构的虚拟机 |
| 收稿时间： | 2014/7/15 0:00:00 |
| 修稿时间： | 2014/10/31 0:00:00 |
Machine-Checked Model for Micro-Dalvik Virtual Machine |
| |
| HE Yan-Xiang,JIANG Nan,LI Qing-An,ZHANG Jun and SHEN Fan-Fan.Machine-Checked Model for Micro-Dalvik Virtual Machine[J].Journal of Software,2015,26(2):364-379. |
| |
| Authors: | HE Yan-Xiang JIANG Nan LI Qing-An ZHANG Jun and SHEN Fan-Fan |
| |
| Affiliation: | Computer School, Wuhan University, Wuhan 430072, China
;State Key Laboratory of Software Engineering Wuhan University, Wuhan 430072, China,Computer School, Wuhan University, Wuhan 430072, China
;Computer School, Hubei University of Technology, Wuhan 430068, China,Computer School, Wuhan University, Wuhan 430072, China
;State Key Laboratory of Software Engineering Wuhan University, Wuhan 430072, China,Computer School, Wuhan University, Wuhan 430072, China
;Software College, East China Institute of Technology, Nanchang 330013, China and Computer School, Wuhan University, Wuhan 430072, China |
| |
| Abstract: | This paper introduces Micro-Dalvik, a formalized Dalvik-like VM model to exhibit core features of the register-based architecture. This formal specification describes the instruction set and runtime state, and the runtime behaviors of the instructions as state transitions based on big-step operational semantics. The Micro-Dalvik VM instruction set is more abstract than comparable Dalvik VM to attain clarity of its semantics, but bears no further simplification of the meaning of instructions. Some properties of Micro-Dalvik VM semantics are stated based on this formal specification and sketch of the proofs is provided. This formalization is implemented in the theorem proof assistant Isabelle/HOL. |
| |
| Keywords: | big-step operational semantics formal verification theorem proving register-based VM |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
