10.3969/j.issn.1000-3428.2008.01.008
一种改进的数据求精证明规则
提出一种改进的数据求精规则,并用关系模式进行描述.引入全局状态来描述程序所有可能的输入和输出,允许非平凡的初始化,允许前向模拟和后向模拟,能应用于消除具体模型的不确定性晚于消除抽象模型的不确定性的情况.并用实例说明了在Isabelle定理证明器中规则的应用方法.
多级安全系统、数据求精、前向模拟、后向模拟
34
TP311(计算技术、计算机技术)
国家重点基础研究发展计划973计划G1999035802
2008-04-15(万方平台首次上网日期,不代表论文的发表时间)
共3页
23-25