基于UML和模型检测的安全模型验证方法

• 作者: 张阳 程亮
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 安全操作系统 系统操作安全 安全策略模型 形式化验证 模型检测 UML
• 年，卷（期）: 2009,（4）
• 页码范围: 699-708
• 页数: 10页
• 分类号: TP309
• 字数: 7686字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2009.00699

摘要

安全策略的形式化分析与验证随着安全操作系统研究的不断深入已成为当前的研究热点之一.文中在总结前人工作的基础上,首次提出一种基于UML和模型检测器的安全模型验证方法.该方法采用UML将安全策略模型描述为状态机图和类图,然后利用转换工具将UML图转化为模型检测器的输入语言,最后由模型检测器来验证安全模型对于安全需求的满足性.作者使用该方法验证了DBLP和SLCF模型对机密性原则的违反.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	程亮	中国科学技术大学电子工程与信息科学系	18	152	6.0	12.0
5	张阳	中国科学院软件研究所信息安全国家重点实验室	53	239	9.0	14.0