摘要: 提出一种改进的数据求精规则,并用关系模式进行描述。引入全局状态来描述程序所有可能的输入和输出,允许非平凡的初始化,允许前向模拟和后向模拟,能应用于消除具体模型的不确定性晚于消除抽象模型的不确定性的情况。并用实例说明了在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
中图分类号:
张 宏;贺也平;石志国;. 一种改进的数据求精证明规则[J]. 计算机工程, 2008, 34(1): 23-25.
ZHANG Hong; HE Ye-ping; SHI Zhi-guo;. Improved Data Refinement Proof Rules[J]. Computer Engineering, 2008, 34(1): 23-25.