Isabelle在分析安全操作系统状态机模型中的应用
文献类型：期刊论文
| 作者 | 陈坤 ; 贺也平 |
| 刊名 | 计算机工程与设计
 |
| 出版日期 | 2008 |
| 卷号 | 29期号:3页码:580-582, 730 |
| 关键词 | 形式化 Isabelle工具 状态机模型 安全操作系统 可信进程模型 |
| 中文摘要 | 为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观．简洁的问题，提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数，以及模型中的安全不变量和状态迁移规 则进行形式化描述的新方法．通过实际验证一种典型的安全操作系统状态机模型——可信进程模型，总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略． |
| 语种 | 中文 |
| 公开日期 | 2010-01-06 |
| 源URL | [http://124.16.136.157/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. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。