计算机工程 ›› 2013, Vol. 39 ›› Issue (5): 318-321.doi: 10.3969/j.issn.1000-3428.2013.05.071

• 开发研究与工程应用 • 上一篇    

基于综合性能的Markov过程验证与分析

纪明宇1,2,王海涛3,陈志远1   

  1. (1. 哈尔滨工程大学计算机科学与技术学院,哈尔滨 150001;2. 东北林业大学信息与计算机工程学院,哈尔滨 150040; 3. 东北农业大学继续教育中心,哈尔滨 150030)
  • 收稿日期:2012-05-07 出版日期:2013-05-15 发布日期:2013-05-14
  • 作者简介:纪明宇(1980-),男,讲师、博士研究生,主研方向:形式化验证,模型检测;王海涛,讲师;陈志远,讲师、博士研究生
  • 基金项目:
    国家自然科学基金资助项目(71001023);中央高校基本科研业务费专项基金资助项目(DL11BB08)

Verification and Analysis of Markov Process Based on Integrated Performance

JI Ming-yu 1,2, WANG Hai-tao 3, CHEN Zhi-yuan 1   

  1. (1. College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China; 2. College of Information and Computer Engineering, Northeast Forestry University, Harbin 150040, China; 3. Continuing Education Center, Northeast Agricultural University, Harbin 150030, China)
  • Received:2012-05-07 Online:2013-05-15 Published:2013-05-14

摘要: 面向复杂信息系统综合性能的形式化验证问题,以数据传输系统为例,使用一种基于改进的马尔可夫判定过程验证分析方法进行复杂信息系统的性能验证。在综合各种连续随机逻辑变体基础上,采用一种表达能力更强的时序逻辑来表示系统模型的复杂性质,运用自动机技术建模路径公式,通过构造积模型完成模型与自动机的同步演化,并给出相应的算法描述。实例结果验证了该方法可有效地扩大模型检测技术的应用范围。

关键词: 综合性能, 形式化验证, 马尔可夫过程, 时序逻辑, 自动机, 积模型

Abstract: Facing the problem of synthesizes performance formal verification for complex information system, this paper uses the data transmission system as example and applies a new property verification method based on improved Markov decision process to verify the performance of the system. A new more expressive temporal logic is used to describe system model properties on the basis of all kinds of continuous stochastic logic variants. By using automata to express logic path formula, the corresponding algorithm is described based on product model which realizes the simultaneous evolution of the model and the automata. Example result verifies the method can effectively expand the application scope of the model checking technology.

Key words: integrated performance, formal verification, Markov process, temporal logic, automata, product model

中图分类号: