|
[1] Wing J M. A symbiotic relationship between formal methods and security //Workshops on Computer Security, Dependability, and Assurance: From Needs to Solutions. Washington, DC, USA: IEEE Computer Society, 1998.
[2] Klein G. Operating system verification—an overview
[J]. Sādhanā, 2009, 34(1): 26-69.
[3] Cock D, Klein G, Sewell T. Secure microkernels, state monads and scalable refinement //Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics. Berlin, Heidelberg: Springer-Verlag, 2008.
[4] Hillebrand M A, Paul W J. On the architecture of system verification environments //Proceedings of the 3rd International Haifa Verification Conference on Hardware and Software: Verification and Testing. Lecture Notes in Computer Science, 4899. Berlin, Germany: Springer-Verlag, 2008.
[5] Hohmuth M, Tews H, Stephens S G. Applying source-code verification to a microkernel: the VFiasco project //Proceedings of the 10th ACM SIGOPS European Workshop. New York, NY, USA: ACM, 2002.
[6] Endrawaty E. Verification of the fiasco IPC implementation . Department of Computer Science, Institute of Theoretical Computer Science. Dresden University of Technology,Germany. 2005.
[7] Clarke E, Grumberg O, Long D. Verification tools for finite-state concurrent systems //A Decade of Concurrency-Reflections and Perspectives. Lecture Notes in Computer Science, 803. London, UK: Springer-Verlag, 1994: 124-175.
[8] Cattel T. Modelization and verification of a multiprocessor realtime OS kernel //Proceedings of FORTE'94. London, UK: Chapman & Hall, Ltd, 1995:55-70.
[9] Duval G, Julliand J. Modelling and verification of the RUBIS μ-kernel with SPIN //SPIN'95. Workshop on Model Checking of Software, 1995.
[10] Tullmann P, Turner J, McCorquodale J, et al. Formal methods: a practical tool for OS implementors //HotOS-VI. Washington, DC, USA: IEEE Computer Society, 1997.
[11] 姜玉蓉. LINUX内核进程间通信的模型检测研究 . 长沙: 湖南大学, 2009.
[12] Universitt Karlsruhe. L4Ka::Pistachio microkernel. http://l4ka.org/projects/pistachio/.
|
