Computer Science ›› 2015, Vol. 42 ›› Issue (8): 203-214.
Previous Articles Next Articles
CHEN Li-rong, LI Yun and LUO Lei
| [1] ISO.ISO 26262-6 Road vehicles－Functional Safety－Part 6:Product development at the software level[S/OL].http://www.iso.org/iso/:ISO,2011 [2] AUTOSAR GbR.Specification of Operating System V4.1.0 R4.0 Rev 2[S/OL].http://www.autosar.org/:AUTOSAR GbR,2011 [3] Klein G.Operating system verification—an overview[J].Sadhana,2009,34(1):27-69 [4] 钱振江,刘苇,黄皓.操作系统形式化设计与验证综述[J].计算机工程,2012,38(11):234-238 Qian Zhen-jiang,Liu Wei,Huang Hao.Survey of formal design and verification for operating system [J].Computer Engineering,2012,38(11):234-238 [5] Elkaduwe D,Klein G,Elphinstone K.Verified protection model of the seL4 microkernel[M]∥Shankar N,Woodcock J,eds.Verified Software:Theories,Tools,Experiments.Springer Berlin Heidelberg,2008:99-114 [6] Heise G,Elphinstone K,Kuz I,et al.Towards trustworthy computing systems:taking microkernels to the next level[J].ACM SIGOPS Operating Systems Review,2007,41(4):3-11 [7] Klein G,Elphinstone K,Heiser G,et al.seL4:Formal verification of an OS kernel[C]∥Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles,2009.Big Sky,MT,USA:ACM,2009:207-220 [8] Schirmer N.Verification of sequential imperative programs in Isabelle-HOL[D].Munich:Technical University Munich,2006 [9] Rieden T I D.Verified linking for modular kernel verification[D].Saarbrucken:Saarland University,2009 [10] Gargano M,Hillebrand M,Leinenbach D,et al.On the correctness of operating system kernels[M]∥Hurd J,Melham T,eds.Theorem Proving in Higher Order Logics.Springer Berlin Heidelberg,2005:1-16 [11] Rieden T I D,Tsyban A.CVM－a verified framework for microkernel programmers[J].Electronic Notes in Theoretical Computer Science,2008,217:151-168 [12] Tsyban A.Formal Verification of a Framework for Microkernel Programmers[D].Saarbrucken:Saarland University,2009 [13] Daum M,Drrenbcher J,Wolff B.Proving fairness and implementation correctness of a microkernel scheduler[J].Journal of Automated Reasoning,2009,42(2-4):349-388 [14] Drrenbcher J.Formal specification and verification of a microkernel[D].Saarbrucken:Saarland University,2010 [15] Schmidt M.Formal verification of a small real-time operating system[D].Saarbrucken:Saarland University,2011 [16] Bogan S.Formal specification of a simple operating system[D].Saarbrucken:Saarland University,2008 [17] Cohen E,Paul W,Schmaltz S.Theory of multi core hypervisor verification[M]∥van Emde Boas P,Groen F,Italiano G,et al,eds.SOFSEM 2013:Theory and Practice of Computer Science.Springer Berlin Heidelberg,2013:1-27 [18] Schmaltz S.Towards the pervasive formal verification of multi-core operating systems and hypervisors implemented in C [D].Saarbrucken:Saarland University,2013 [19] Baumann C,Bormer T,Blasum H,et al.Proving memory separation in a microkernel by code level verification[C]∥ 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops(ISORCW),2011.IEEE,2011:25-32 [20] 陈超超,曾庆凯.采用SPIN的L4内存管理形式化验证[J].计算机工程,2009,35(11):131-133 Chen Chao-chao,Zeng Qing-kai.Formal verification of L4 memory management using SPIN [J].Computer Engineering,2009,35(11):131-133 [21] 钱振江,刘苇,黄皓.操作系统对象语义模型(OSOSM)及形式化验证[J].计算机研究与发展,2012,49(12):2702-2712 Qian Zhen-jiang,Liu Wei,Huang Hao.OSOSM:operating system object semantics model and formal verification [J].Journal of Computer Research and Development,2012,49(12):2702-2712 [22] 李康杰,钱振江,黄皓.微内核中断机制的形式化设计与验证[J].计算机科学,2013,40(3):197-200,205 Li Kang-jie,Qian Zhen-jiang,Huang Hao.Formal design and verification of interrupt mechanism based on microkernel [J].Computer Science,2013,40(3):197-200,205 [23] 钱振江.安全操作系统形式化设计与验证方法研究[D].南京:南京大学,2013 Qian Zhen-jiang.Research on methodology of Formal design and verification for security operating system [D].Nanjing:Nanjing University,2013 [24] 程亮.基于模型检测的安全操作系统验证方法研究[D].合肥:中国科学技术大学,2009 Cheng Liang.Research on verification of secure operating system based on model checking [D].Hefei:University of Science and Technology of China,2009 [25] 吴丹,刘芳,戴葵,等.Linux中System V进程通信机制安全性形式化验证[J].计算机工程与科学,2002,24(2):13-18 Wu Dan,Liu Fang,Dai Kui,et al.The formal verification of safety in System V of Linux [J].Computer Engineering & Science,2002,24(2):13-18 [26] 李斌.基于B的安全操作系统原型的形式化分析和验证[D].昆明:云南大学,2011 Li Bin.Formal analysis and verification of secure operating system prototype based on B [D].Kunming:Yunnan University,2011 [27] 张忠秋,董云卫,张雨,等.基于Coq的微内核操作系统程序验证方法研究[J].计算机测量与控制,2011,19(8):1939-1942 Zhang Zhong-qiu,Dong Yun-wei,Zhang Yu,et al.Research on microkernel operating system program verification based on Coq [J].Computer Measurement & Control,2011,19(8):1939-1942 [28] 顾飞.共享内存IPC机制的形式化验证与实现[D].兰州:兰州大学,2012 Gu Fei.Formal verification and implementation of shared memory IPC mechanism [D].Lanzhou:Lanzhou University,2012 [29] Shi Jian-qi,Zhu Hui-biao,He Ji-feng,et al.ORIENTAIS:Formal verified OSEK/VDX real-time operating system [C]∥IEEE International Conference on Engineering of Complex Computer Systems, 2012.Los Alamitos,CA,USA:IEEE Computer Society,2012:293-301 [30] 彭云辉.基于AUTOSAR的汽车电子操作系统及其应用的建模与分析[D].上海:华东师范大学,2014 Peng Yun-hui.Modeling and analysis of AUTOSAR OS and application [D].Shanghai:East China Normal University,2014 [31] Alkassar E,Bhme S,Mehlhorn K,et al.Verification of certifying computations[M]∥Gopalakrishnan G,Qadeer S,eds.Computer Aided Verification.Springer Berlin Heidelberg,2011:67-82 [32] Alkassar E,Hillebrand M A,Paul W J,et al.Automated verification of a small hypervisor[M]∥Leavens G,O’Hearn P,Rajamani S, eds.Verified Software:Theories,Tools,Experiments.Springer Berlin Heidelberg,2010:40-54 [33] Shadrin A.Mixed low-and high level programming language semantics and automated verification of a small hypervisor[D].Saarbrucken:Saarland University,2012 [34] The OSEK/VDX Group.OSEK/VDX Operating System specification Version 2.2.3[S/OL].http://www.osek-vdx.org/:The OSEK/VDX Group,2005 [35] AUTOSAR GbR.Technical Safety Concept Status Report V1.0.0 R4.0 Rev 1[S/OL].http://www.autosar.org/:AUTOSAR GbR,2009 [36] 陈丽蓉,燕立明,罗蕾.汽车电子嵌入式操作系统的隔离保护机制[J].电子科技大学学报,2014,43(3):450-456 Chen Li-rong,Yan Li-ming,Luo Lei.An isolation and protection mechanism of automotive electronic embedded operating system [J].Journal of University of Electronic Science and Technology of China,2014,43(3):450-456 [37] Alkassar E,Bhme S,Mehlhorn K,et al.A Framework for the Verification of Certifying Computations[J].Journal of Automated Reasoning,2014,52(3):241-273 |
| No related articles found! |
|
||
Home