Page 72 - 《软件学报》2021年第6期

1646 Journal of Software 软件学报 Vol.32, No.6, June 2021

[8] Jiang JJ, Qiao L, Yang MF, Yang H, Liu B. Operating system task management requirements layer modeling and verification based
on Coq. Ruan Jian Xue Bao/Journal of Software, 2020,31(8):2375−2387 (in Chinese with English abstract). http://www.jos.org.cn/
1000-9825/5961.htm [doi: 10.13328/j.cnki.jos.005961]
[9] Regehr J, Cooprider N. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 2007,
174(9):139−150. [doi: 10.1016/j.entcs.2007.04.002]
[10] Cui J, Duan ZH, Tian C, Zhang N. Modeling and analysis of nested interrupt systems. Ruan Jian Xue Bao/Journal of Software,
2018,29(6):1670−1680 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5472.htm [doi: 10.13328/j.cnki.jos.
005472]
[11] Liu H, Zhang H, Jiang Y, et al. iDola: Bridge modeling to verification and implementation of interrupt-driven systems. In: Proc. of
the Theoretical Aspects of Software Engineering Conf. (TASE). IEEE, 2014. 193−200. [doi: 10.1109/TASE.2014.33]
[12] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183−235.
[13] Zhou XY, Gu B, Zhao JH, Yang MF, Li XD. Model checking technique for interrupt-driven system. Ruan Jian Xue Bao/Journal of
Software, 2015,26(9):2212−2230 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4713.htm [doi: 10.13328/j.
cnki.jos.004713]
[14] Najumudheen ESF, Mall R, Samanta D. Modeling and coverage analysis of programs with exception handling. In: Proc. of the 12th
Innovations on Software Engineering Conf., Formerly Known as India Software Engineering Conf. (ISEC 2019). Article 15. New
York: Association for Computing Machinery, 2019. 1−11. [doi: https://doi.org/10.1145/3299771.3299785]
[15] Robillard MP, Murphy GC. Static analysis to support the evolution of exception structure in object-oriented systems. ACM Trans.
on Softw. Eng. Methodol, 2003,12(2):191−221. [doi: https://doi.org/10.1145/941566.941569]
[16] Harr R, Kaptelinin V. Interrupting or not: Exploring the effect of social context on interrupters’ decision making. In: Proc. of the
7th Nordic Conf. on Human-Computer Interaction: Making Sense through Design (NordiCHI 2012). New York: Association for
Computing Machinery, 2012. 707−710. [doi: https://doi.org/10.1145/2399016.2399124]
[17] Sozeau M, Boulier S, Forster Y, Tabareau N, Winterhalter T. Coq Coq correct! Verification of type checking and erasure for Coq,
in Coq. In: Proc. of the ACM Program. Lang. 4, POPL, Article 8. 2020. 28. [doi: https://doi.org/10.1145/3371076]
[18] Yang YX, Xu YY, Li JL, Yang C. Progress and performance evaluation of Bei Dou global navigation satellite system: Data
analysis based on BDS-3 demonstration system. Scientia Sinica (Terrae), 2018,48(5):584−594 (in Chinese with English abstract).

附中文参考文献:
[1] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33−61. http://www.jos.org.cn/1000-9825/5652.htm [doi:
10.13328/j.cnki.jos.005652]
[7] 乔磊,杨孟飞,谭彦亮,蒲戈光,杨桦.基于 Event-B 的航天器内存管理系统形式化验证.软件学报,2017,28(5):1204−1220. http://
www.jos.org.cn/1000-9825/5218.htm [doi: 10.13328/j.cnki.jos.005218]
[8] 姜菁菁,乔磊,杨孟飞,杨桦,刘波.基于 Coq 的操作系统任务管理需求层建模及验证.软件学报,2020,31(8):2375−2387. http://www.
jos.org.cn/1000-9825/5961.htm [doi: 10.13328/j.cnki.jos.005961]
[10] 崔进,段振华,田聪,张南.一种嵌套中断系统的建模和分析方法.软件学报,2018,29(6):1670−1680. http://www.jos.org.cn/1000-
9825/5472.htm [doi: 10.13328/j.cnki.jos.005472]
[13] 周筱羽,顾斌,赵建华,杨孟飞,李宣东.中断驱动系统模型检验.软件学报,2015,26(9):2212−2230. http://www.jos.org.cn/1000-9825/
4713.htm [doi: 10.13328/j.cnki.jos.004713]
[18] 杨元喜,许扬胤,李金龙,杨诚.北斗三号系统进展及性能预测——实验验证数据分析.中国科学(地球科学),2018,48(5):584−594.

马智(1994－),男,博士生,主要研究领域为 杨孟飞(1962－),男,博士,研究员,博士生
空间飞行器嵌入式系统,控制系统,总体 导师,CCF 高级会员,主要研究领域为空间
技术. 飞行器嵌入式系统,控制系统,总体技术.

乔磊(1982－),男,博士,研究员,CCF 专业 李少峰(1992－),男,博士生,主要研究领域
会员,主要研究领域为操作系统模型设计, 为操作系统内存管理,文件系统.
存储系统,文件系统.