| Isabelle在分析安全操作系统状态机模型中的应用 |
| |
| 引用本文： | 陈坤,贺也平.Isabelle在分析安全操作系统状态机模型中的应用[J].计算机工程与设计,2008,29(3):580-582,730. |
| |
| 作者姓名： | 陈坤 贺也平 |
| |
| 作者单位： | 1. 中国科学院研究生院,北京,100080;中国科学院软件研究所,基础软件工程技术中心,北京,100080
2. 中国科学院软件研究所,基础软件工程技术中心,北京,100080 |
| |
| 基金项目： | 国家自然科学基金
,
北京市自然科学基金 |
| |
| 摘 要： | 为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观、简洁的问题,提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数,以及模型中的安全不变量和状态迁移规则进行形式化描述的新方法.通过实际验证一种典型的安全操作系统状态机模型--可信进程模型,总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略.
|
| 关 键 词： | 形式化 Isabelle工具 状态机模型 安全操作系统 可信进程模型 |
| 文章编号： | 1000-7024（2008）03-0580-03 |
| 收稿时间： | 2007-03-21 |
| 修稿时间： | 2007年3月21日 |
Application of Isabelle in analyzing secure operating system state-machine models |
| |
| CHEN Kun,HE Ye-ping.Application of Isabelle in analyzing secure operating system state-machine models[J].Computer Engineering and Design,2008,29(3):580-582,730. |
| |
| Authors: | CHEN Kun HE Ye-ping |
| |
| Abstract: | The existing formal frame for state-machine model has trouble in concisely and specifically analyzing secure operating system state-machine models. To solve this problem, a method of using Isabelle to formally describe types, variables, constants, relations, mappings and functions in secure operating system state-machine models and secure invariants and state transition operations in the models is introduced. Thenaftertheverificationofarepresentativemodeltrustedprocessmodel, an effective strategy ofIsabelle assisted formal design, analysis, verification of secure operating system state-machine models is concluded. |
| |
| Keywords: | formalization Isabelle state machine secure operating system model trusted process model |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
