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

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

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

CLC Number: 

• TP311