%0 Journal Article
%T 基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究
%A 崔隽
%A 黄皓
%A 陈志贤
%J 计算机科学
%D 2010
%I 
%X 隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.
%K 不干扰模型
%K 进程隔离
%K 通信顺序进程
%K 形式化验证
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=A27969396E77104CA937D84F87399DB7&yid=140ECF96957D60B2&vid=42425781F0B1C26E&iid=B31275AF3241DB2D&sid=2922B27A3177030F&eid=E2546871E5B846EF&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=13