期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

一个机器检测的Micro-Dalvik虚拟机模型 被引量：5

Machine-Checked Model for Micro-Dalvik Virtual Machine
下载PDF
导出
摘要 给出了一个寄存器架构的虚拟机模型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 Miero-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.
作者 何炎祥 江南 李清安 张军 沈凡凡
机构地区 武汉大学计算机学院 软件工程国家重点实验室(武汉大学) 湖北工业大学计算机学院 东华理工大学软件学院
出处 《软件学报》 EI CSCD 北大核心 2015年第2期364-379,共16页 Journal of Software
基金 国家自然科学基金(91118003 61170022)
关键词 大步操作语义 形式化验证 定理证明 寄存器架构的虚拟机 big-step operational semantics formal verification theorem proving register-based VM
分类号 TP303 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献31

  • 1McCarthy J, Painter J. Correctness of a compiler for arithmetic expression. In: Proc. of the IFTP Congress. 1967.21-28.
  • 2Nipkow T, Paulson CL, Wenzel M. A Proof Assistant for Higher-Order Logic. Berlin, Heidelberg: Springer-Verlag, 2010.
  • 3Paller G. Dalvik opcodes, http://pallergabor.uw.hu/androidblog/dalvik_opeode:.html.
  • 4Xu C, He YX, Wu W, Chen Y, Liu JB. Verifying implementation correctness of compiling optimization based on simulation relation. Chinese Journal of Electronics, 2012,40(11): 2171-2176 (in Chinese with English abstract). [doi: 10.3969/j.issn.0372- 2112.2012.11.005].
  • 5Nipkow T, Klein G. Concrete semantics--A proof assistant approach. Technical Report. http://www21.in.tum.de/-nipkow/ Concrete-Semantics.
  • 6Payet 1, Spoto F. An operational semantics of android activities. In: Proc. of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation. New York: ACM Press, 2014. 121-132. [doi: 10.1145/2543728.2543748].
  • 7徐超,何炎祥,吴伟,陈勇,刘健博.基于模拟关系的编译优化实现正确性验证方法[J].电子学报,2012,40(11):2171-2176. 被引量：2
  • 8Alves-Foss J. Formal syntax and semantics of java. LNCS 1523, New York: Springer-Verlag, 1999.
  • 9Barthe G, Dufay G, Jakubiec L, Serpette B, Sousa SM. Formal executable semantics of the JavaCard platform. In: Sands D, ed. Proc. of the Programming Languages and Systems Conf. New York: Springer-Verlag, 2001. 302-319. [doi: I 0.I 007/3-540-45309- 1_20].
  • 10Android. Bytecode for the Dalvik VM. http://surce'andridcm/tech/dalvilddalvik-bytecdehtml.

二级参考文献59

  • 1胡定磊,陈书明.低功耗编译技术综述[J].电子学报,2005,33(4):676-682. 被引量：11
  • 2唐遇星,邓鹍,周兴铭.基于Trace-Cache的多级动态优化框架设计[J].电子学报,2005,33(11):1946-1951. 被引量：4
  • 3胡定磊,陈书明,王凤芹,刘春林.基于互补谓词的编译优化[J].电子学报,2006,34(7):1280-1286. 被引量：2
  • 4张焕国,罗捷,金刚,朱智强,余发江,严飞.可信计算研究进展[J].武汉大学学报（理学版）,2006,52(5):513-518. 被引量：114
  • 5Department of Defense. DoD 5200.28-STD Department of defense trusted computer system evaluation criteria[S]. USA: DoD, 1985.
  • 6Winskel G. The Formal Semantics of Programming Languages [M]. London: The MIT Press, 1993:10-50.
  • 7Tennent R D, Ghica D R. Abstract models of storage [J]. Higher-Order and Symbolic Computation, 2000, 13 ( 1 ) : 119-129.
  • 8Bertot Y, Casteran P. Interactive Theorem Proving and Program Development [M]. New York: Springer, 2004: 10- 120.
  • 9Kernighan B W, Ritchie D M. The C Programming Language[M]. New York: Prentice Hall, 1989:1-300.
  • 10Hoare C A R. An axiomatic loasis for computer programming [J]. Communications of the ACM, 1969, 12(10): 576 -580.

共引文献14

同被引文献54

  • 1BALASANGAMESHWARA J, RAJU N. A hybrid policymr fault tolerant load balancing in Grid computing environ-ments[J]. Journal of Network and computer Applications,2012.35(1), 412-22.
  • 2Boyle MJ, Resler DR, Winter LV. Do you trust your com- piler [ J ]. Computer, 1999,32 (5) :65-73.
  • 3Stepney S. High Integrity Compilation:A Case Study[ M]. Haffield: Prentice Hall Intemational(UK) Ltd, 1993.
  • 4McCarthy J, Painter J. Correctness of a compiler for arith- metic expression [ A ]. Proceedings of the Symposium in Applied Mathematics[ C]. Rhode Island, USA, 1967. 33 -41.
  • 5Plotldn DG. The Origins of structural operational semantics[J ]. The Journal of Logic and Algebraic Programming, 2004,6:3 - 15.
  • 6Morris LF. Advice on structuring compilers and proving them correct[ A]. Proceedings of the 1 st Annual ACM SI- GACT-SIGPLAN Symposium on Principles of Program- ming Languages ( POPL' 73 ) [ C ]. Boston: ACM Press, 1973. 144 - 152.
  • 7Zadamowski P. C lambda calculus & compiler verification [ D]. Sydney :University of New South Wales ,2011.
  • 8Burstall MR. Proving properties of programs by structural induction[ J]. The Computer Journal, 1969, 12 ( 1 ) : 41 -48.
  • 9Nipkow T, Paulson CL, Wenzel M. A Proof for Higher- Order Logic [ M]. Berlin: Springer-Verlag, 2010.
  • 10Yves B, Pierre C. Interactive Theorem Proving and Pro- gram Development: Coq' Art: the Calculus of Inductive Constructions [ M ]. Berlin: Springer-Verlag,2004.

引证文献5

二级引证文献11

软件学报
2015年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部