基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究 (2010年)

隔离有助于阻止信息泄露或被篡改、错误或失败被传递等。利用不干扰理论给出了隔离的精确语义，以利于分析和制定系统的隔离策略；利用通信顺序进程CSP来定义上述隔离语义，并给出一个系统满足给定隔离策略的判定断言，以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证。以基于虚拟机的文件服务监控器为例，展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略。