%0 Journal Article
%T Formal Design and Verification of Interrupt Mechanism Based on Microkernel<br>微内核中断机制的形式化设计与验证
%A 李康杰
%A 钱振江
%A 黄皓
%J 计算机科学
%D 2013
%I 
%X It is difficult to describe the correctness and security of the operate system (OS) by quantitative analysis. Formal method is the acknowledged standard one in design and verification for OS. Based on the operate system object semantics model (OSOSM) , we designed and verified the interruption mechanism of microkernel architecture using for- mal method,which was realized on our self-implemented verified trusted operate system (VTOS). Meanwhile,we used the theorem prover Isabelle/HOI. to formally describe the design process, and verify the integrality of the interruption mechanism of VTOS. Our research plays certain referential significance on formal design and verification of OS.
%K Formal design
%K Formal verification
%K Microkernel
%K Interrupt
%K Integrity<br>形式化设计，形式化验证，微内核，中断，完整性
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=EEFFAAE7C668ACD136C3F3767676F4DB&yid=FF7AA908D58E97FA&vid=1371F55DA51B6E64&iid=38B194292C032A66&sid=2BA123C6EB9D54C2&eid=1E41DF9426604740&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=0