Page 97 - 《软件学报》2021年第7期

安冬冬 等:不确定环境下 hCPS 系统的形式化建模与动态验证 2015

[37] Vardi MY. Automatic verification of probabilistic concurrent finite state programs. Foundations of Computer Science, 1985,
327–338. [doi: 10.1109/SFCS.1985.12]
[38] Vardi MY, Wolper P. An automata theoretic approach to automatic program verification. In: Proc. of the 1st Symp. on Logic in
Computer Science. IEEE Computer Society, 1986. 322–331.
[39] Courcoubetis C, Yannakakis M. The complexity of probabilistic verification. Journal of the ACM, 1995,42(4):857–907. [doi: 10.
1145/210332.210339]
[40] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real time systems. In: Proc. of the Int’l Conf. on
Computer Aided Verification (CAV). 2011. 585–591. [doi: 10.1007/978-3-642-22110-1_47]
[41] Kwiatkowska M, Norman G, Parker D. Probabilistic symbolic model checking with prism: A hybrid approach. Int’l Journal on
Software Tools for Technology Transfer, 2001. [doi: 10.1007/s10009-004-0140-2]
[42] Kwiatkowska M. Quantitative verification: Models techniques and tools. In: Proc. of the 6th Joint Meeting of the European
Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering. 2007. 449–458. [doi: 10.
1145/1295014.1295018]
[43] Hartmanns A, Hermanns H. The modest toolset: An integrated environment for quantitative modelling and verification. In: Proc. of
the Int’l Conf. on Toolsand Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2014. 593–598. [doi: 10.
1007/978-3-642-54862-8_51]
[44] Katoen JP, Zapreev IS, Hahn EM, et al. The ins and outs of the probabilistic model checker MRMC. Performance Evaluation, 2011,
68(2):90–104. [doi: 10.1016/j.peva.2010.04.001]
[45] Hensel C, Junges S, Katoen J, et al. The probabilistic model checker storm. CoRR, 2020, abs/2002.07080.
[46] Dehnert C, Junges S, Katoen JP, Volk M. A storm is coming: A modern probabilistic model checker. In: Proc. of the Int’l Conf. on
Computer Aided Verification (CAV). 2017. [doi: 10.1007/978-3-319-63390-9_31]
附中文参考文献:
[4] 孙海英.基于多形态时钟输入输出迁移系统的安全软件测试研究[博士学位论文].上海:华东师范大学,2017.
[16] 杜德慧,程贝,刘静.面向安全攸关系统中小概率事件的统计模型检测.软件学报,2015,26(2):305−320. http://www.jos.org.cn/
1000-9825/4783.htm [doi: 10.13328/j.cnki.jos.004783]
[18] 杜德慧,昝慧,姜凯强,程贝.一种面向 CPS 的自适应统计模型检测方法.软件学报,2017,28(5):1128–1143. http://www.jos.org.cn/
1000-9825/5216.htm [doi: 10.13328/j.cnki.jos.005216]

安冬冬(1990－),女,博士,CCF 专业会员, 陈小红(1982－),女,博士,副教授,CCF 专
主要研究领域为形式化建模与验证,统 业会员,主要研究领域为需求工程,形式
计模型检测,人机物融合系统,自动驾驶 化方法,安全攸关系统.
系统.

刘静(1964－),女,博士,教授,博士生导师, 孙海英(1976－),女,博士,讲师,CCF 专业
CCF 专业会员,主要研究领域为基于模型 会员,主要研究领域为形式化建模,形式
的高可信软件开发技术,形式化方法建模 化验证,基于形式化的测试.
与验证.