| 基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究 |
| |
| 引用本文： | 崔隽,黄皓,陈志贤.基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究[J].计算机科学,2010,37(6):147-154. |
| |
| 作者姓名： | 崔隽 黄皓 陈志贤 |
| |
| 作者单位： | 1. 南京大学软件新技术国家重点实验室,南京,210093;南京大学计算机科学与技术系,南京,210093
2. 南京大学软件新技术国家重点实验室,南京,210093;南京大学计算机科学与技术系,南京,210093;南京工业大学信息学院,南京,210009 |
| |
| 基金项目： | 863国家高技术研究发展计划 |
| |
| 摘 要： | 隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.
|
| 关 键 词： | 不干扰模型 进程隔离 通信顺序进程 形式化验证 |
| 收稿时间： | 2009/9/20 0:00:00 |
| 修稿时间： | 2009/10/27 0:00:00 |
| 本文献已被 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
