参考文献
[1] 林惠民, 张文辉. 模型检测: 理论、方法与应用[J]. 电子学报, 2002, 30(S1): 1907-1912.
[2] 钮 俊, 曾国荪, 王 伟. 基于模型检测的时间空间性能验证方法[J]. 计算机学报, 2010, 33(9): 1621-1633.
[3] 周从华, 刘志锋, 王昌达. 概率计算树逻辑的限界模型检 测[J]. 软件学报, 2012, 23(7): 1656-1668.
[4] Hermanns H, Kwiatkowska M, Norman G, et al. On the Use of MTBDDs for Performability Analysis and Veri?cation of Stochastic Systems[J]. Journal of Logic and Algebraic Programming, 2003, 56(1/2): 23-67.
[5] Donaldson A F, Miller A. Symmetry Reduction for Pro- babilistic Model Checking Using Generic Representatives[C]// Proc. of the 4th International Conference on Automated Technology for Verification and Analysis. [S. l.]: Springer- Verlag, 2006: 9-23.
[6] Kwiatkowska M, Norman G, Parker D. Symmetry Reduction for Probabilistic Model Checking[C]//Proc. of the 18th International Conference on Computer Aided Verification. Seattle, USA: Springer-Verlag, 2006: 7-20.
[7] Pekergin N, Younes S. Stochastic Model Checking with Stochastic Comparison[C]//Proc. of European Performance Engineering Workshop. Berlin, Germany: Springer-Verlag, 2005: 109-123.
[8] Zhang Lijun, Jansen D N, Nielson F, et al. Automata-based CSL Model Checking[C]//Proc. of the 38th International Colloquium on Automaton, Languages and Programming. Berlin, Germany: Springer-Verlag, 2011: 271-282.
[9] Desharnais J, Gupta V, Jagadeesan R, et al. Weak Bisi- mulation is Sound and Complete for PCTL*[J]. Information and Computation, 2010, 208(2): 203-219.
[10] 聂锡宁, 蔡国永. Petri网的重写逻辑模型及其属性验证[J]. 桂林电子科技大学学报, 2011, 31(3): 208-212.
[11] 李力行, 金 芝, 李 戈. 基于时间自动机的物联网服务建模和验证[J]. 计算机学报, 2011, 34(8): 1366-1377.
[12] 王 聪, 王智学. 基于自动机理论的UML活动图模型检验方法[J]. 系统仿真学报, 2007, 19(22): 5311-5314.
[13] 雷丽晖, 段振华. 一种基于扩展有限自动机验证组合Web服务的方法[J]. 软件学报, 2007, 18(12): 2980-2990.
编辑 顾逸斐 |