摘要
面向复杂信息系统综合性能的形式化验证问题,以数据传输系统为例,使用一种基于改进的马尔可夫判定过程验证分析方法进行复杂信息系统的性能验证。在综合各种连续随机逻辑变体基础上,采用一种表达能力更强的时序逻辑来表示系统模型的复杂性质,运用自动机技术建模路径公式,通过构造积模型完成模型与自动机的同步演化,并给出相应的算法描述。实例结果验证了该方法可有效地扩大模型检测技术的应用范围。
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.
出处
《计算机工程》
CAS
CSCD
2013年第5期318-320,F0003,共4页
Computer Engineering
基金
国家自然科学基金资助项目(71001023)
中央高校基本科研业务费专项基金资助项目(DL11BB08)
关键词
综合性能
形式化验证
马尔可夫过程
时序逻辑
自动机
积模型
integrated performance
formal verification
Markov process
temporal logic
automata
product model