| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 基于UML和模型检测的安全模型验证方法 |
| 作者 | 程亮1),2) 张阳2) |
| 作者单位 | 1)(中国科学技术大学电子工程与信息科学系 合肥 230027) 2)(中国科学院软件研究所信息安全国家重点实验室 北京 100190) |
| 发表年份 | 2009 |
| 发表月份 | 4期(699—708) |
| 文章摘要 | 摘要 安全策略的形式化分析与验证随着安全操作系统研究的不断深入已成为当前的研究热点之一.文中在总结前人工作的基础上，首次提出一种基于UML和模型检测器的安全模型验证方法.该方法采用UML将安全策略模型描述为状态机图和类图，然后利用转换工具将UML图转化为模型检测器的输入语言，最后由模型检测器来验证安全模型对于安全需求的满足性.作者使用该方法验证了DBLP和SLCF模型对机密性原则的违反. 关键词 安全操作系统；系统操作安全；安全策略模型；形式化验证；模型检测；UML 中图法分类号: TP309 DOI号: 10.3724/SP.J.1016.2009.00699 |