中国科学院机构知识库网格
Chinese Academy of Sciences Institutional Repositories Grid
一种改进的数据求精证明规则

文献类型:期刊论文

作者张宏 ; 贺也平 ; 石志国
刊名计算机工程
出版日期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
其他版本

除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。