扩展不干扰模型(ENISM)及基于CSP的描述和验证方法

作     者：崔隽 黄皓 高晓春 CUI Jun;HUANG Hao;GAO Xiao-Chun

作者机构：南京大学软件新技术国家重点实验室南京210093 南京大学计算机科学与技术系南京210093 

基　　金：国家"八六三"高技术研究发展计划项目基金(2007AA01Z409) 国家自然科学基金(60473093)资助~~ 

出 版 物：《计算机学报》 (Chinese Journal of Computers)

年 卷 期：2010年第33卷第5期

页      码：877-889页

摘      要：在不干扰理论的基础上,提出扩展不干扰模型ENISM及其验证方法,用以描述和分析操作系统中的信息流策略.工作包括:(1)依据系统功能模块定义多个执行域,以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础;(2)给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC;(3)基于通信顺序进程给出ENISM-CC的语义及操作系统模块设计的形式化描述和验证方法.

主 题 词：不干扰模型 通信顺序进程 形式化描述 形式化验证 完整性 

学科分类：0810[工学-土木类] 0808[工学-自动化类] 0839[0839] 08[工学] 0835[0835] 0811[工学-水利类] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3724/sp.j.1016.2010.00877

馆 藏 号：203111786...