关键词: 不干扰模型，进程隔离，通信顺序进程，形式化验证

Abstract: Processes or modules isolation helps protect information from being revealed or modified and prevent processes or modules from passing error or failure to others. We proposed the semantics of isolation by noninterference theory,for the purpose of analyzing and designing isolation strategies in software systems;we also specified the semantics of isolation and its determine conditions by Communicating Sequential Process(CSP) in order for automated formal verificanon of isolation strategics in systems in formal verification tool FDR2. And in this paper, with an example of file system monitor in a virtual machine, we illustrated how to specify a system or a isolation strategy by CSP formulation and how to verify given isolation strategics in a system automatically in FDR2.

Key words: Nonintcrfcrcncc modcl,Proccsscs isolation,Communicating scqucntial proccsscs,Formal verification