期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到1篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
基于HyperLTL模型检测技术的K步不透明性验证
1
作者 任翔 王子佩 +1 位作者 张佳慧 韩晓光 《天津科技大学学报》 2025年第3期65-71,共7页
不透明性是一种重要的信息流安全属性,用于表征不同动态系统中各种安全和隐私需求。在离散事件系统中,K步不透明性刻画的是入侵者无法根据当前的输出观测序列确定系统是否在K个观测步之内曾访问过秘密状态。HyperLTL作为一种在形式化验... 不透明性是一种重要的信息流安全属性,用于表征不同动态系统中各种安全和隐私需求。在离散事件系统中,K步不透明性刻画的是入侵者无法根据当前的输出观测序列确定系统是否在K个观测步之内曾访问过秘密状态。HyperLTL作为一种在形式化验证中表达信息流属性的工具,已被证明可以采用一个统一的Kripke结构分别验证初始状态不透明性、当前状态不透明性和无限步不透明性,但并未涉及K步不透明性。针对HyperLTL模型的K步不透明性验证问题,通过添加Sink状态释放了对原系统的限制性条件,进一步构造改进的Kripke结构并给出K步不透明性在HyperLTL中的判据,即验证原系统在HyperLTL语义下是否满足K步不透明性。 展开更多
关键词 离散事件系统 K步不透明性 hyperltl 改进的Kripke结构 Sink状态
在线阅读 下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部