Guo Liang. Reconstructing the kernel of SZRTOS rea-l tim e OS in XYZ/E[ D]. Be ijing: Institute o f Softw are, Ch inese Academy of Sc ience, 2002. ( in Ch inese)
[4]
[ Fo rd R L. Specification-based A tom ic ityTesting o f theMK + + K ernel[ R ]. Cambr idge, MA: TheOpen G roup Resea rch Inst-itute, 1997.
[5]
[ Cattel T. M odelization and V erification of a Mu ltiprocessor Rea l T im e OS Kerne l[ C ] / / Proceedings of FORTE 94. Sw itzerland:B ern, 1994.
[6]
[ Bev ierW R. A ve rified operating sy stem kerne l[ D]. Austin: University of Texas, 1987.
[7]
[ B ev ierW R. KIT: a study in operating system ver ifica tion[ J]. IEEE T ransOn Softw are Eng ineer ing, 1989, 15( 11): 1 382-1 396.
[8]
[ Shap iro J S, W ebe r S. Ve rify ingOpera ting Sy stem Secur ity, MS- C IS97- 26[ R]. Philadelph ia, PA: University o f Pennsy-lvania, 1995.
Zhu Xueyang, Tang Zhisong. A tem po ra l log ic-based softw are arch itecture description language XYZ /ADL [ J]. Softw are,2003, 14( 4): 713-720. ( in Ch inese)
Zhang Guangquan. Softw are arch itecture re finem ent form onitor system s based on tem pora l log ic language[ J]. Com puter Engineering and App lica tions, 2003, 39( 31): 14-17. ( in Ch inese)
[13]
[ Roger S Pressman. 软件工程――实践者的研究方法[M ]. 黄柏素, 梅宏, 译. 北京: 机械工业出版社, 1999.
[14]
Roger S Pressman. So ftw are Eng ineer ing――A Prac titioner. s Approach[M ]. H uang Ba isu, M e iHong, T ransla ted. Be ijing:ChinaM ach ine Press, 1999. ( in Ch inese)
[15]
[ W ing JM. A spec ifier. s introduction to form a lm ethods[ J]. IEEE Com puter, 1990, 23( 9): 8-24.
[16]
[ 唐稚松. 时序逻辑程序设计与软件工程( 上册) [M ] . 北京: 科学出版社, 2002.
[17]
Tang Zh isong. Sequential Log ic Programm ing and So ftwa re Eng ineering[M ] . Beijing: Sc ience Press, 2002. ( in Ch inese)
[18]
[ M cDouga ll R ichard, M auro Jim. So lar is 内核结构[M ] . 北京: 机械工业出版社, 2007.M cDouga ll R ichard, M auro Jim. So lar is In ternals[M ]. Be ijing: Ch inaM ach ine Press, 2007. ( in Ch inese)
[19]
[ Love Robe rt. L inux内核设计与实现[M ]. 陈莉君, 译. 北京: 机械工业出版社, 2006.
