一种改进的数据求精证明规则
文献类型:期刊论文
作者 | 张宏 ; 贺也平 ; 石志国 |
刊名 | 计算机工程
![]() |
出版日期 | 2008 |
卷号 | 34期号:1页码:23-25 |
关键词 | 多级安全系统 数据求精 前向模拟 后向模拟 multilevel secure system data refinement forward simulation backward simulation |
ISSN号 | 1000-3428 |
其他题名 | improved data refinement proof rules |
中文摘要 | 提出一种改进的数据求精规则,并用关系模式进行描述。引入全局状态来描述程序所有可能的输入和输出,允许非平凡的初始化,允许前向模拟和后向模拟,能应用于消除具体模型的不确定性晚于消除抽象模型的不确定性的情况。并用实例说明了在Isabelle定理证明器中规则的应用方法。 |
收录类别 | wanfang,cscd,cnki |
语种 | 中文 |
公开日期 | 2010-08-23 |
附注 | 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. |
源URL | [http://124.16.136.157/handle/311060/3748] ![]() |
专题 | 软件研究所_基础软件国家工程研究中心_期刊论文 |
推荐引用方式 GB/T 7714 | 张宏,贺也平,石志国. 一种改进的数据求精证明规则[J]. 计算机工程,2008,34(1):23-25. |
APA | 张宏,贺也平,&石志国.(2008).一种改进的数据求精证明规则.计算机工程,34(1),23-25. |
MLA | 张宏,et al."一种改进的数据求精证明规则".计算机工程 34.1(2008):23-25. |
入库方式: OAI收割
来源:软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。