Isabelle在分析安全操作系统状态机模型中的应用

	Isabelle在分析安全操作系统状态机模型中的应用
	陈坤; 贺也平
	2008
发表期刊	计算机工程与设计
卷号	29 期号:3 页码:580-582, 730
摘要	为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观．简洁的问题，提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数，以及模型中的安全不变量和状态迁移规则进行形式化描述的新方法．通过实际验证一种典型的安全操作系统状态机模型——可信进程模型，总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略．
关键词	形式化 Isabelle工具状态机模型安全操作系统可信进程模型
语种	中文
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/644
专题	基础软件国家工程研究中心
推荐引用方式 GB/T 7714	陈坤,贺也平. Isabelle在分析安全操作系统状态机模型中的应用[J]. 计算机工程与设计 ,2008,29(3):580-582, 730.
APA	陈坤,&贺也平.(2008).Isabelle在分析安全操作系统状态机模型中的应用.计算机工程与设计 ,29(3),580-582, 730.
MLA	陈坤,et al."Isabelle在分析安全操作系统状态机模型中的应用".计算机工程与设计 29.3(2008):580-582, 730.