Computer Science ›› 2010, Vol. 37 ›› Issue (6): 147-154.
Previous Articles Next Articles
CUI Jun,HUANG Hao,CHEN Zhi-xian
Online:
Published:
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
CUI Jun,HUANG Hao,CHEN Zhi-xian. Research on Isolation Semantics Description Based on Noninterference Theory and Automated Isolation Strategy Verification Scheme[J].Computer Science, 2010, 37(6): 147-154.
0 / / Recommend
Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks
URL: https://www.jsjkx.com/EN/
https://www.jsjkx.com/EN/Y2010/V37/I6/147
Cited