基于自动机的概率计算树逻辑验证方法

根据带有随机特征的复杂信息系统性质验证的需求,针对离散概率回报模型的分层直到公式,提出一种性质验证分析方法。在综合各种离散随机逻辑的基础上,使用一种同时具有迁移回报及迁移步区间表达能力的概率计算树逻辑表示系统模型的分层直到路径公式性质,使用自动机技术建模路径公式,通过构造积模型完成模型与自动机的同步演化,基于积模型给出相应的状态概率满足算法。实例结果验证了该方法的可行性和有效性。     

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.     

构建度量区时序逻辑的时间自动机

在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。     

一类时间自动机的时间约束可满足性判定方法

时间自动机是一种有效描述实时系统行为的计算模型。借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性。在此过程中对时间自动机的验证是非常关键的一步。验证的主要目的是为了保证时间自动机能够正确地描述实时系统。其中迁移的时间约束可满足性就是需要验证的性质之一。常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大。该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数。     

Spark环境下基于SMT的分布式限界模型检测

在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。     

概率时段演算的模型检验概述

在实际工程应用中,越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模,概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时,作为时段演算的一种扩展,概率时段演算被用来计算此类系统满足需求的概率。该文主要概述基于概率时间自动机的概率时段演算的模型检验主要步骤及其核心算法,其中模型检验的核心算法通过分别将前两者转换为区域图和概率分支时间逻辑来达成。     

概率时段演算的模型检验概述

在实际工程应用中,越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模,概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时,作为时段演算的一种扩展,概率时段演算被用来计算此类系统满足需求的概率。该文主要概述基于概率时间自动机的概率时段演算的模型检验主要步骤及其核心算法,其中模型检验的核心算法通过分别将前两者转换为区域图和概率分支时间逻辑来达成。     

改进的验证正确性ACTL性质的限界模型检测方法

近些年来,基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充,已经得到了一定的发展。其中,大部分的研究成果都集中在了使用该方法来进行系统查错方面,而在正确性性质的验证上一直难有突破,原因在于正确性性质的验证依赖于一个完备上界,而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变,就能够在一定程度上解决这一问题,进行正确性性质的验证。在此基础上对该编码方法进行改进,从而提高它的求解效率,扩大其应用领域。     

基于一阶迁移系统的限界模型检测工具实现

为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力.然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证.结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示.     

概率计算树逻辑的限界模型检测

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

一种基于时间自动机的实时系统模型检查算法的设计与实现

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用Visual C++语言描述了实时特性验证中的数据结构,实现了实时特性验证算法,实验表明利用该算法可以进行实时系统的形式化验证。     

实时并发系统的PTSL模型检测

随着实时并发系统的软件规模越来越大、复杂性日趋增加,如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质,它不仅包括对系统模型的遍历以及基于图形的分析方法,而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型（CGS）的扩展,在此基础上添加了概率与时间性质,提出了概率时间并发博弈结构（PTCGS）。同时本文还提出了新的逻辑语言-概率时间策略逻辑（PTSL）,它显式地把策略作为一阶逻辑中的对象,从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求,从而提高系统的可靠性。最后,本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。     

一种基于优先级扩展的时间自动机模型中DBM减法算法的改进

本文介绍一种具有优先级扩展的时间自动机模型,并对一种计算DBM减法算法进行改进。这种减法是DBM上操作中的一种,它会产生需要用DBM集来表示的非凸集合。DBM的数量影响符号模型检测的性能,我们的减法算法是有效的,因为它产生的DBM的数量相对于最初算法具有较大程度的约减。DBM减法操作扩展了具有优先级的时间自动机理论,它对对于具有紧急行为的变换描述、死锁检测、时间博弈等问题具有非常重要的作用。     

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.     

时间自动机可达性分析算法的改进

模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。     

对时间自动机进行空性检测的过程和改进

为了提高对时间自动机进行空性检测的效率,研究了使用基于时钟区域(zone)的符号化方法和抽象对时间自动机进行空性检测,提出了针对时间自动机自身特点对检测过程进行改进的方法.通过使用基于zone的符号化表示方法和抽象,一个符号化状态表示显式的状态的集合,时间自动机的状态空间会显著缩小,不同的抽象方法对状态空间有不同的效果.符号化状态间不仅有相等关系还有包含关系,通过判断这种包含关系可以尽早的找到接收路径和避免不必要的状态展开从而提高空性检测的效率.实现了改进的检测过程,对一些例子进行了数据比较,取得了较好的实验结果.     

一种基于离散时间自动机的LTL性质检测工具

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.     

基于概率时间自动机的异构多agent自适应运行时验证

多agent自适应系统在运行过程中需要根据环境进行自适应调整。异构agent能够提高agent的使用效率和降低系统的构建成本,但存在复杂的协作问题,因此提出一种基于概率时间自动机的异构多agent自适应系统运行时验证方法。该方法通过形式化描述异构agent的功能特征并融合环境中的随机因素构建概率时间自动机模型模拟自适应系统的运行过程;针对异构agent之间的协作逻辑制定安全约束条件以确保系统运行中状态迁移流程的安全性。通过模型检查结合运行时定量验证方法进行实验验证,在智能泊车系统案例中应用该方法。实验结果表明,agent之间协作逻辑的正确性可以有效保证系统运行时的稳定性,且相较于不使用运行时定量验证的初始系统在相同时间内正常运行的时间提升了21%左右。