| 一种改进的数据求精证明规则 |
| |
| 引用本文： | 张宏,贺也平,石志国.一种改进的数据求精证明规则[J].计算机工程,2008,34(1):23-25. |
| |
| 作者姓名： | 张宏 贺也平 石志国 |
| |
| 作者单位： | 1. 中国科学院软件研究所,北京,100080;中国科学院研究生院,北京,100049
2. 中国科学院软件研究所,北京,100080 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划) |
| |
| 摘 要： | 提出一种改进的数据求精规则，并用关系模式进行描述。引入全局状态来描述程序所有可能的输入和输出，允许非平凡的初始化，允许前向模拟和后向模拟，能应用于消除具体模型的不确定性晚于消除抽象模型的不确定性的情况。并用实例说明了在Isabelle定理证明器中规则的应用方法。
|
| 关 键 词： | 多级安全系统 数据求精 前向模拟 后向模拟 |
| 文章编号： | 1000-3428（2008）01-0023-03 |
| 收稿时间： | 2007-02-07 |
| 修稿时间： | 2007年2月7日 |
Improved Data Refinement Proof Rules |
| |
| ZHANG Hong,HE Ye-ping,SHI Zhi-guo.Improved Data Refinement Proof Rules[J].Computer Engineering,2008,34(1):23-25. |
| |
| Authors: | ZHANG Hong HE Ye-ping SHI Zhi-guo |
| |
| Affiliation: | ZHANG Hong1,2, HE Ye-ping1, SHI Zhi-guo1,2 |
| |
| 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. |
| |
| Keywords: | multilevel secure system data refinement forward simulation backward simulation |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
|
