Institutional Repository
| Isabelle在分析安全操作系统状态机模型中的应用 | |
| 陈坤; 贺也平 | |
| 2008 | |
| Source | 计算机工程与设计
 |
| Volume | 29Issue:3Pages:580-582, 730 |
| English Abstract | 为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观．简洁的问题，提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数，以及模型中的安全不变量和状态迁移规 则进行形式化描述的新方法．通过实际验证一种典型的安全操作系统状态机模型——可信进程模型，总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略． |
| Keyword | 形式化 Isabelle工具 状态机模型 安全操作系统 可信进程模型 |
| Language | 中文 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/644 |
| Collection | 基础软件国家工程研究中心 |
| Recommended Citation 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. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 陈坤-per.pdf（360KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment