主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
何炎祥,江南,李清安,张军,沈凡凡.一个机器检测的Micro-Dalvik虚拟机模型.软件学报,2015,26(2):364-379
一个机器检测的Micro-Dalvik虚拟机模型
Machine-Checked Model for Micro-Dalvik Virtual Machine
投稿时间:2014-07-15  修订日期:2014-10-31
DOI:10.13328/j.cnki.jos.004787
中文关键词:  大步操作语义  形式化验证  定理证明  寄存器架构的虚拟机
英文关键词:big-step operational semantics  formal verification  theorem proving  register-based VM
基金项目:国家自然科学基金(91118003, 61170022)
作者单位E-mail
何炎祥 武汉大学 计算机学院, 湖北 武汉 430072
软件工程国家重点实验室武汉大学, 湖北 武汉 430072 
 
江南 武汉大学 计算机学院, 湖北 武汉 430072
湖北工业大学 计算机学院, 湖北 武汉 430070 
nanjiang@whu.edu.cn 
李清安 武汉大学 计算机学院, 湖北 武汉 430072
软件工程国家重点实验室武汉大学, 湖北 武汉 430072 
 
张军 武汉大学 计算机学院, 湖北 武汉 430072
东华理工大学 软件学院, 江西 南昌 330013 
 
沈凡凡 武汉大学 计算机学院, 湖北 武汉 430072  
摘要点击次数: 2937
全文下载次数: 2497
中文摘要:
      给出了一个寄存器架构的虚拟机模型Micro-Dalvik,包括虚拟机指令集和虚拟机运行时状态的形式化,并以大步操作语义(big-step operational semantics)的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换.最后,以定理的形式描述了语义满足的性质,并得到证明.这个模型的指令集包括了大部分Dalvik虚拟机指令,为获得形式语义的清晰化,它在Dalvik VM指令集上进行了必要的抽象,对其实质没有改变,因而具有较大的实用性.该形式化模型通过了定理证明助手Isabelle/HOL的验证.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利