Bounded Model Checking of PTACTL Based on SMT

doi:10.3969/j.issn.1006-2475.2016.03.009

Abstract

Abstract: Probabilistic timed automata are an extension of timed automata with discrete transition probabilities, and can be used to model timed randomized protocols or fault-tolerant systems. We present a bounded model checking method on SMT for verifying probabilistic timed automata against PTACTL properties. This method adds the transition times and transition probabilities into the ACTL properties and changes the encodings of models and properties in order to verify them, which is come from the SMT-based bounded model checking. We also give two examples to show that this method is effectiveness and efficiency.

Key words: bounded model checking, probabilistic timed systems, probabilistic timed automata, PTACTL, SMT

CLC Number:

TP301

MAO Liang-wen1, XU Liang2,3. Bounded Model Checking of PTACTL Based on SMT[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2016.03.009.

References

[1] Penczek W, Wozna B, Zbrzezny A. Towards bounded model checking for the universal fragment of TCTL[C]// Proceedings of the 2002 Formal Techniques in Real-time and Fault-tolerant Systems. 2002:265-288.

[2] Yu Fang, Wang Bow-Yaw, Huang Yao-Wen. Bounded model checking for region automata[C]// Proceedings of the 2004 Formal Techniques, Modeling and Analysis of Timed and Fault-tolerant Systems. 2004:246-262.

[3] Alur R, Courcoubetis C, Dill D. Model-checking in dense real-time[J]. Information and Computation, 1993,104(1):2-34.

[4] Markey N, Schnoebelen P. Symbolic model checking for simply-timed systems[C]// Proceedings of the 2004 Formal Techniques, Modeling and Analysis of Timed and Fault-tolerant Systems. 2004:102-117.

[5] 徐亮,陈伟,徐艳艳,等. Improved bounded model checking for the universal fragment of CTL[J]. 计算机科学技术学报(英文版), 2009,24(1):96-109.

[6] 徐亮. 改进的以SMT为基础的实时系统限界模型检测[J]. 软件学报, 2010,21(7):1491-1502.

[7] 徐亮,刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. 计算机工程与科学, 2013,35(10):166-171.

[8] Kwiatkowska M, Norman G, Parker D. A framework for verification of software with time and probabilities[C]// Proceedings of the 2010 Formal Modeling and Analysis of Timed Systems. 2010:25-45.

[9] Berendsen J, Jansen D N, Vaandrager F. Fortuna: Model checking priced probabilistic timed automata[C]// Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST). 2010:273-281.

[10] Norman G, Parker D, Sproston J. Model checking for probabilistic timed automata[J]. Formal Methods in System Design, 2013,43(2):164-190.

[11] Brazdil T, Brozek V, Forejt V, et al. Branching-time model-checking of probabilistic pushdown automata[J]. Journal of Computer & System Sciences, 2014,80(1):139-156.

[12] Kwiatkowska M, Norman G, Sproston J, et al. Symbolic model checking for probabilistic timed automata[J]. Information and Computation, 2007,205(7):1027-1077.

[13] Dang Van Hung, Zhang Miaomiao. On verification of probabilistic timed automata against probabilistic duration properties[C]// Proceedings of the 13th IEEE International Conference on Embedded and Real-time Computing Systems and Applications. 2007:165-172.

[14] Clarke Jr E M, Grumberg O, Peled D A. Model Checking[M]. MIT Press, 1999.

[15] Penczek W, Wozna B, Zbrzezny A. Bounded model checking for the universal fragment of CTL[J]. Fundamenta Informaticae, 2002,51(1):135-156.

[16] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems[C]// Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’ 11). 2011:585-591.

[17] Katoen J, Zapreev I, Hahn E M, et al. The ins and outs of the probabilistic model checker MRMC[C]// Proceedings of the 6th International Conference on Quantitative Evaluation of Systems (QEST’ 09). 2009:167-176.

[18] Rote G. Crossing the bridge at night[J]. Bulletin of the European Association for Theoretical Computer Science, 2002(78):241-246.

[19] Franklin J D. Abstractions for Model Checking System Security[R]. CMU-CS-12-113, Carnegie Mellon University, 2012.

[20] de Moura L, Rueß H, Sorea M. Bounded model checking and induction: From refutation to verification[C]// Proceedings of the 2003 International Conference on Computer Aided Verification (CAV’ 03). 2003:14-26.

[21] McMillan K L. Interpolation and SAT-based model checking[C]// Proceedings of the 2003 International Conference on Computer Aided Verification (CAV’ 03). 2003:1-13.