《计算机学报》文章摘要   全文下载
文章题目	扩展不干扰模型(ENISM)及基于CSP的描述和验证方法
作者	崔隽 黄皓 高晓春
作者单位	1)(南京大学软件新技术国家重点实验室 南京 210093) 2)(南京大学计算机科学与技术系 南京 210093)
发表年份	2010
发表月份	5期(877—889)
文章摘要	摘要 在不干扰理论的基础上，提出扩展不干扰模型ENISM及其验证方法，用以描述和分析操作系统中的信息流策略.工作包括：(1)依据系统功能模块定义多个执行域，以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础；(2)给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC；(3)基于通信顺序进程给出ENISM-CC的语义及操作系统模块设计的形式化描述和验证方法. 关键词 不干扰模型；通信顺序进程；形式化描述；形式化验证；完整性 中图法分类号 TP309 DOI号: 10.3724/SP.J.1016.2010.00877