An approach of model checking time or space performance

被引：0
|
作者：
Niu J. [1 ,2 ,3 ]
Zeng G.-S. [1 ,2 ]
Wang W. [1 ,2 ]
机构：
[1] Department of Computer Science and Technology, Tongji University
[2] Embedded System and Service Computing Key Laboratory of Ministry of Education
[3] College of Information Engineering, Zhejiang Business Technology Institute
来源：
Jisuanji Xuebao/Chinese Journal of Computers | 2010年 / 33卷 / 09期
关键词：
Duality; Model checking; Nondeterminism; Reachability probabilities; Time or space performance;
D O I：
10.3724/SP.J.1016.2010.01621
中图分类号：
学科分类号：
摘要：
It has been a research focus that the performance analysis of complex systems such as network protocols which include nondeterministic choices. Besides time, space aspect is also considered during the process of performance evaluation. By model checking, we can verify whether time or space performance meets expected constraints. The authors adopt CTMRP (Continuous-Time Markov Reward Process) as the verification model since it can depict nondeterminism intuitively. The temporal logic CSRL (Continuous Stochastic Reward Logic) is extended by replacing path operators with regular expressions in order to express more comprehensive time or spatial properties which are based on states or paths. For deterministic schedulers, a duality result of constrained reachability probabilities between time and space is proposed, and its correctness is proved based on the existing work. Based on the theoretical consequences, the verification of space performance is reduced to the corresponding analysis of time reachability. The model checking algorithm and a new approach for the performance evaluation of complex systems are given.
引用
收藏
页码：1621 / 1633
页数：12
相关论文
共 28 条
  • [1] Lin C., Li Y.-J., Wang Z.-M., Status and development of formal methods for performance evaluation, Acta Electronica Sinica, 30, 12 A, pp. 1917-1922, (2002)
  • [2] Lin C., Lei L., Research on next generation internet architecture, Chinese Journal of Computers, 30, 5, pp. 693-711, (2007)
  • [3] Guo B., Shen Y., Shao Z.-L., The redefinition and some discussion of green computing, Chinese Journal of Computers, 32, 12, pp. 2311-2319, (2009)
  • [4] Cloth L., Katoen J.-P., Khattri M., Pulungan R., Model checking Markov reward models with impulse rewards, Proceedings of the International Conference on Dependable Systems and Networks (DSN'05), pp. 722-731, (2005)
  • [5] Hermanns H., Interactive Markov chains, (1998)
  • [6] Johr S., Model checking compositional Markov systems, (2007)
  • [7] Baier C., Haverkort B., Hermanns H., Katoen J.-P., On the logical characterisation of performability properties, Proceedings of the ICALP 2000: Automata, Languages and Programming, pp. 780-792, (2000)
  • [8] Haverkort B., Cloth L., Hermanns H., Katoen J.-P., Baier C., Model checking performability properties, Proceedings of the DSN 2002, pp. 103-112, (2002)
  • [9] Niu J., Zeng G.-S., Chen B., An integrated verification model atsFPM based on functional, time and spatial constraints, Chinese Journal of Computers, 32, 4, pp. 740-750, (2009)
  • [10] Baier C., Pedro D., Marcus G., Partial order reduction for probabilistic branching time, Electronic Notes in Theoretical Computer Science, 153, 2, pp. 97-116, (2006)
123