随机模型检测连续时间Markov过程

功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度,对复杂并发系统进行功能验证和性能分析,统一地评估系统是否可信。连续时间Markov决策过程CTMDP(Continuous time Markov decision process)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用CTMDP作为系统定性验证和定量分析模型,将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解,并证明验证过程的正确性,最终借助模型检测器MRMC(Markov Reward Model Chcckcr)实现模型检测。理论分析表明,提出的针对CI'MDP模型的验证需求是必要的,验证思路和方法具有可行性。     

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

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

基于SMT的PTACTL限界模型检测方法

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。     

有界模型检测和串空间模型相结合的安全协议验证

提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显.     

基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.     

基于时间自动机模型的测试用例生成方法优化

为了减少测试产生、执行,存储以及维护测试用例的代价,提出了一种基于时间自动机模型的测试用例生成方法的优化技术.针对实时系统中不同的时间尺度,为了加快基于模型的测试用例生成的速度,通过对原时间自动机模型的结构进行改进,对这类实时系统进行测试产生优化.实验结果表明,优化后产生的测试用例集的大小及所用时间相对于优化之前有较大程度的约减,为进一步减少测试执行的时间,提高测试效率,加快软件开发进程提供了可行的解决途径.     

基于时间STM的软件形式化建模与验证方法

状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.     

基于着色时间Petri网的工作流模型及其性能分析

为了将着色时间Petri网的并行式工作流模型应用于产品数据管理系统,在工作流建模阶段对工作流的静态和动态结构性能加以分析.采用活动扫描法作为工作流系统行为的仿真策略,研究了工作流模型到着色时间工作流网模型的转换过程.给出了用可达图检验工作流程中是否存在死锁和陷阱的判定定理.以一种循环组件的或分支跳出并行流程的审批工作流为例,对论述的定理和方法进行了分析和验证.     

基于词对向量空间模型的新事件检测方法

新事件检测（NED）的目标是从一个或多个新闻源中检测出报道一个新闻话题的第一个新闻。传统向量空间模型采用单个词来表示文本特征,考虑到词的位置信息以及其他的表示内容的信息,提出了词对表示文本的方法,并结合HowNet资源对所抽取的词对进行归一化处理,最后对不同类别新闻中不同词性对的权重参数进行优化。通过在已有的突发性新闻语料上进行实验,表明这种改进方法的效果比较明显,性能也有一定的提高。     

UML Statecharts的模型检验方法

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.     

A Partial Order Approach to Branching Time Logic Model Checking

Partial order techniques enable reducing the size of the state space used for model checking, thus alleviating the “state space explosion” problem. These reductions are based on selecting a subset of the enabled operations from each program state. So far, these methods have been studied, implemented, and demonstrated for assertional languages that model the executions of a program as computation sequences, in particular the linear temporal logic. The present paper shows, for the first time, how this approach can be applied to languages that model the behavior of a program as a tree. We study here partial order reductions for branching temporal logics, e.g., the logics CTL and CTL* (with the next time operator removed) and process algebra logics such as Hennesy–Milner logic (withτactions). Conditions on the selection of subset of successors from each state during the state-space construction, which guarantee reduction that preserves CTL* properties, are given. The experimental results provided show that the reduction is substantial.     

A Partial Approach to Model Checking

This paper presents a model-checking method for linear-time temporal logic that can avoid most of the state explosion due to the modeling of concurrency by interleaving. The method relies on the concept of Mazurkiewicz′s trace as a semantic basis and uses automata-theoretic techniques, including automata that operate on words of ordinality higher than ω.     

Model Checking Quantitative Linear Time Logic

This paper considers QLtl, a quantitative analagon of Ltl and presents algorithms for model checking QLtl over quantitative versions of Kripke structures and Markov chains.     

一种面向CPS的自适应统计模型检测方法

随着计算机与物理环境的交互日益密切,信息物理融合系统（cyber physical systems,CPSs）在健康医疗、航空电子、智能建筑等领域有着广泛的应用前景,CPSs的正确性、可靠性分析已引起人们的广泛关注.统计模型检测（statistical model checking,SMC）技术能够对CPSs进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPSs的效率,是目前所面临的主要困难之一.针对此问题,本文首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法（Bayesian Interval Estimate,BIE）在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用了主成分分析、前缀树约减等技术,对仿真路径进行学习和抽象,以减少样本空间.接着,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题.最后,结合经典案例进行实验分析,实验结果表明自适应SMC算法框架能够在一定误差范围内有效提高CPSs统计模型检测的效率,为CPSs的分析验证提供了一种有效的途径.     

Model Checking Semi-Continuous Time Models Using BDDs

The verification of timed systems is extremely important, but also extremely difficult. Several methods have been proposed to assist in this task, including extensions to symbolic model checking. One possible use of model checking to analyze timed systems is by modeling passage of time as the number of taken transitions and applying quantitative algorithms to determine the timing parameters of the system. The advantage of this method is its simplicity and efficiency. In this paper we extend this technique in two ways. First, we present new quantitative algorithms that are more efficient than their predecessors. The new algorithms determine the number of occurrences of events in all paths between a set of starting states and a set of final states. We then use these algorithms to introduce a new model of time, in which the passage of time is dissociated from the occurrence of events. With this new model it is possible to verify systems that were previously thought to require dense time models. We use the new method to verify two such examples previously analyzed by the HyTech tool: a steam boiler example and a fuel injection controller.     

Software Model Checking: The VeriSoft Approach

Verification by state-space exploration, also often referred to as model checking, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communication protocols). Unfortunately, traditional model checking is restricted to the verification of properties of models, i.e., abstractions, of concurrent systems.We discuss in this paper how model checking can be extended to analyze arbitrary software, such as implementations of communication protocols written in programming languages like C or C++. We then introduce a search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code.During the past five years, VeriSoft has been applied successfully for analyzing several software products developed in Lucent Technologies, and has also been licensed to hundreds of users in industry and academia. We discuss applications, strengths and limitations of VeriSoft, and compare it to other approaches to software model checking, analysis and testing.     

An Approach to Concurrent Control Flow Checking

A control flow checking scheme capable of detecting control flow errors of programs resulting from software coding errors, hardware malfunctions, or memory mutilation during the execution of the program is presented. In this approach, the program is partitioned into loop-free intervals and a database containing the path information in each of the loop-free intervals is derived from the detailed design. The path in each loop-free interval actually traversed at run time is recorded and then checked against the information provided in the database, and any discrepancy indicates an error. This approach is general, and can detect all uncompensated illegal branches. Any uncompensated error that occurs during the execution of a loop-free interval and manifests itself as a wrong branch within the loop-free interval or right after the completion of execution of the loop-free interval is also detectable. The approach can also be used to check the control flow in the testing phase of program development. The capabilities, limitations, implementation, and the overhead of using this approach are discussed.