作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2008, Vol. 34 ›› Issue (1): 23-25. doi: 10.3969/j.issn.1000-3428.2008.01.008

• 博士论文 • 上一篇    下一篇

一种改进的数据求精证明规则

张 宏1,2,贺也平1,石志国1,2   

  1. (1. 中国科学院软件研究所,北京 100080;2. 中国科学院研究生院,北京 100049)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-01-05 发布日期:2008-01-05

Improved Data Refinement Proof Rules

ZHANG Hong1,2, HE Ye-ping1, SHI Zhi-guo1,2   

  1. ZHANG Hong1,2, HE Ye-ping1, SHI Zhi-guo1,2
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-01-05 Published:2008-01-05

摘要: 提出一种改进的数据求精规则,并用关系模式进行描述。引入全局状态来描述程序所有可能的输入和输出,允许非平凡的初始化,允许前向模拟和后向模拟,能应用于消除具体模型的不确定性晚于消除抽象模型的不确定性的情况。并用实例说明了在Isabelle定理证明器中规则的应用方法。

关键词: 多级安全系统, 数据求精, 前向模拟, 后向模拟

Abstract: This paper presents an improved data refinement proof rules. These rules are formulated on relations, including a global state to describe all possible input and output for programs, allowing non-trivial initialization, allowing both forward and backward simulations. These rules are also applicable when the non-determinism resolution in the concrete model is later than in the abstract model. In addition, it uses a simple example to illustrate the application of the rules in Isabelle theorem prover.

Key words: multilevel secure system, data refinement, forward simulation, backward simulation

中图分类号: