并发反应式系统的组合模型检验与组合精化检验

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题。针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法。根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型。利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例。实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题。     

一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题.针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法.根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型.利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例.实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题.     

对VIS系统关键技术的改进

本文在分析形式化验证 /综合系统VIS的基础上 ,改进了此系统中的关键技术———二叉判定图 (BDD) ,使BDD能表示电路的定时性质 ,这样就为VIS系统能够进行电路的时间特性验证和实时模型检验打下了基础。     

基于抽象和组合方法的网络协议验证

由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。     

用VIS系统验证电路的实时特性的探讨

文章在分析形式化验证／综合系统VIS 的基础上,改进了该电子系统中的关键技术——二叉判定图（BDD）,使BDD能表示电路的定时性质,这样就为VIS系统能够进行电路的时间特性验证和实时模型检验打下了基础。     

构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.     

一种针对CP-nets并发模型的验证方法

状态爆炸问题导致CP-nets并发模型的正确性验证工作十分困难。提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正。这在一定程度上避免了状态爆炸问题并实现了模型验证。通过将上述方法应用于HMIPv6协议模型,验证了其有效性。     

测试目的引导的模型检测方法与技术研究

为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储。然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换。其次利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述。最后使用模型检测工具验证被测程序是否满足测试目的。实验结果表明,测试目的引导的模型检测方法能够实现对伪代码的模型检测并且可以缓解状态空间爆炸问题。     

基于分段模型检测的云服务跨域认证协议的形式化分析与验证

针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。     

任务流模型检验的研究

对任务流模型检验技术进行了讨论。任务流方法不关心状态数量、能否从一个指定状态到达另一指定状态及系统必须的状态是否存在,而是关心状态组合提供的功能是否存在及各状态组合之间是否存在指定的转换关系,从而避免了状态空间爆炸问题。模块搜索算法以模块为基础对任务流模型进行搜索来验证给定系统是否满足规范要求。     

Symbolic model checking for self-stabilizing algorithms

A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors     

Heuristic search + local model checking in selective mu-calculus

Many tools for the automatic analysis or verification of finite-state distributed systems are based on construction of the global state graph of the system under consideration. Thus, they often fail because of the state explosion problem: the state space of a distributed system potentially increases exponentially in the number of its parallel components. To overcome this problem, we present a model checking procedure, based on the combination of heuristic searches with ideas taken from local model checking. We use heuristic mechanisms for exploration of the search space in order to avoid construction of the complete state graph.     

Syntactic reductions for efficient deadlock analysis

A well‐known problem in the verification of concurrent systems based on model checking is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. A reduction technique to reduce state explosion in deadlock checking is presented. The method is based on an automatic syntactic simplification of a calculus of communicating systems (CCS) specification, which keeps the parts of the program structure that may lead to a deadlock and deletes the other parts. Copyright © 2002 John Wiley & Sons, Ltd.     

基于层次单元划分的软件模型检测技术研究

通过对近年来软件模型检测领域流行的几种技术进行综述,提出了一种基于层次单元划分,使用引导式搜索方式的软件模型检测方案。本方案分为预处理、单元划分、状态空间搜索三个阶段,其中使用on-the-fly技术提高了搜索性能。实验证明,该方案在解决状态爆炸问题上有较好的效果。     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

面向随机模型检验的模型抽象技术

随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓解状态空间爆炸问题的重要技术之一,已经开始被应用到随机模型检验领域并取得了一定的进展.以面向随机模型检验的模型抽象技术为研究对象,首先给出了模型抽象技术的问题描述,然后按抽象模型构造技术分类归纳了其研究方向及目前的研究进展,最后对比了目前的模型抽象技术及其关系,总结出其还未能给出模型抽象问题的满意答案,并指出了有效解决模型抽象问题未来的研究方向.