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

Improved Data Refinement Proof Rules

作　　者：张宏[1] 贺也平[1] 石志国[1] 

机构地区：[1]中国科学院软件研究所

出　　处：《计算机工程》2008年第1期23-25,共3页Computer Engineering

基　　金：国家“973”计划基金资助项目(G1999035802)

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]