参考文献/References:
[ 1] Roger S Pressman. 软件工程——实践者的研究方法[M ]. 黄柏素, 梅宏, 译. 北京: 机械工业出版社, 1999.
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)
[ 2] W ing JM. A spec ifier. s introduction to form a lm ethods[ J]. IEEE Com puter, 1990, 23( 9): 8-24.
[ 3] 唐稚松. 时序逻辑程序设计与软件工程( 上册) [M ] . 北京: 科学出版社, 2002.
Tang Zh isong. Sequential Log ic Programm ing and So ftwa re Eng ineering[M ] . Beijing: Sc ience Press, 2002. ( in Ch inese)
[ 4] 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)
[ 5] Love Robe rt. L inux内核设计与实现[M ]. 陈莉君, 译. 北京: 机械工业出版社, 2006.
Love Robe rt. L inux Kerne l Deve lopm ent[M ] . Chen Lijun, T ransla ted. Be ijing: Ch inaM ach ine Press, 2006. ( in Ch inese)
[ 6] 郭亮. 基于XYZ /E重构SZRTOS实时操作系统内核[ D]. 北京: 中国科学院软件技术研究所, 2002.
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)
[ 7] 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.
[ 8] 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.
[ 9] Bev ierW R. A ve rified operating sy stem kerne l[ D]. Austin: University of Texas, 1987.
[ 10] 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.
[ 11] 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.
[ 12] 朱雪阳, 唐稚松. 其于时序逻辑的软件结构描述语言XYZ/ADL[ J] . 软件学报, 2003, 14( 4): 713-720.
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)
[ 13] 张广泉. 基于时序逻辑语言描述的监控系统的软件体系结构求精[ J]. 计算机工程与应用, 2003, 39( 31): 14-17.
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)