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

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