一种基于Event-B语言的时间触发系统建模方法

安全关键信息物理系统的时间属性建模和验证至关重要。Event-B模型验证避免了基于状态遍历模型检查方法的状态空间爆炸问题，验证时耗少，适用于高并发系统。然而，常规的Event-B方法缺乏时间语义表达结构，特别是缺乏对可提高系统可预测性的时间触发属性的支持。首先，介绍支持时间触发系统的抽象建模框架TTEB,从系统行为和实现2个抽象层次对时间属性进行建模和精化。然后，通过有序事件链组成的时间触发转移描述行为层时间触发属性；通过全局时钟到分布式本地时钟的精化和分解实现行为模型到实现模型的转化；运用时间触发转移建模分布式时钟周期同步。最后，基于从车跟车系统建模与验证说明方法的可用性和有效性。     

模型检测中虚假反例检测方法

抽象技术是解决模型检测状态空间爆炸的一种有效方法,但其中一个重大的障碍是对系统的抽象会引入原始系统中本来不存在的行为,即可能会引入虚假反例。因此,需要根据反例对抽象模型进行精化。如何判定一个反例是虚假反例还是真实反例,在抽象精化过程中相当重要。本文根据状态的前驱和后继定义失效状态,给出虚假反例的定义,并基于此提出检测虚假反例的并行算法。     

构件组合的集成测试

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

基于UML的作战系统概念模型六元抽象描述

系统六元抽象分析方法,从系统的范畴、系统的组元、系统的结构、系统的状态、系统的运行和系统的功能六个方面对系统进行抽象描述,它对作战系统的抽象更具准确性和完备性。文章通过分析系统概念模型的任务空间、实体、状态、结构、行为和交互的内涵以及UML图形表示法的特征,在概念模型同UML表示法之间建立对应关系。     

构件组合的集成测试

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

基于完备抽象解释的性质强保留抽象研究

在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ-演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全抽象.然后基于抽象解释框架及完备抽象解释和性质强保留之间的关系,构造使得Lμ性质强保留的最小抽象模型精化,并转换为抽象解释中抽象域的最小完备精化.依据此完备抽象域求得性质强保留的最优抽象状态划分,从而构造出性质强保留且最优的抽象状态转换系统.     

参数化系统二维抽象的理论基础

模型之间的等价关系和抽象模型的性质保持是保证验证正确的必要条件,参数化系统二维抽象从构成系统状态空间的二维方向分别进行抽象,证明了此抽象方法的正确性和合理性,即TDA模型与原始模型存在模拟关系,而且在TDA模型中成立的只对单个变量进行全称量化的单索引ACTL*公式,在任意规模的原始模型中也成立,为简化参数化系统验证提供了理论依据。     

面向参数化系统验证的自动抽象方法

针对参数化系统验证面临的状态空间爆炸问题,提出自动抽象方法化简参数化系统状态空间.首先进行Y-抽象建立单进程有限状态机模型,然后通过对多个Y-抽象模型的合成运算得到异步合成的参数化系统,最后根据定义的谓词对参数化系统进行X-抽象得到二维抽象模型.运用该方法,对基于Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly和Dragon的7个参数化协议和注入错误的MESI协议进行自动化抽象建模,并验证了相关性质,有效地提升了验证参数化系统的能力、缩短了验证时间;应用文中方法验证FT-1000CPU的一致性协议的结果表明,该方法在降低验证复杂度方面具有明显优势.     

基于行为的可信动态度量的状态空间约简研究

针对复杂并发计算机系统行为可信的动态度量研究中,细粒度动态度量所引发的状态空间爆炸问题一直是研究的难点.文中基于并发理论研究复杂并发计算机系统行为可信问题,在保障度量可靠性的前提下对系统状态空间进行约简,即通过标记变迁系统模型描述行为系统,通过事件结构模型研究行为关系,依据行为关系对变迁系统中各条路径进行重构,合并重构路径中相同的路径,实现变迁关系集约简,缩小状态空间.通过上述方法缓解了状态空间爆炸,并且,根据约简后的状态空间得到面向行为的可信动态度量的行为预期,增加细粒度动态度量方法在复杂系统中应用的可行性.     

定性推理在矩形phase—portrait近似中的应用

抽象近似是验证混合系统安全性的主要方法,矩形phase-portrait近似是通过构造简单的线性混合自动机来近似原混合自动机.phase-portrait近似的关键步骤是如何划分状态空间.本文采用定性推理的方法,叙述了如何根据系统动态特征来划分状态空间及如何精化抽象模型.     

一种基于模型检测的二进制程序脆弱性分析框架

针对二进制程序脆弱性分析的实际需求,提出了一种基于模型检测的二进制程序脆弱性分析框架。首先定义了二进制程序的抽象模型,描述了基于有限状态自动机的软件脆弱性形式化表示和基于事件系统的软件安全属性表示方法。在此基础上,提出了基于模型检测的脆弱性分析过程和算法。根据该分析框架,设计并实现了二进制程序脆弱性分析工具原型。通过脆弱性分析实验,详细说明了该框架的工作原理,验证了该分析方法的有效性。     

模型检验中抽象技术研究综述

在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论了抽象技术今后的发展方向。     

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

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

基于抽象和搜索空间划分的安全性判定方法

为满足访问控制策略安全性快速判定的要求,提出一种基于谓词抽象和验证空间划分的访问控制策略状态空间约减方法,将在访问控制策略原始状态机模型上的安全性分析工作转移到包含较少状态的抽象模型上,并进一步划分抽象模型的验证空间,以提高效率。理论分析和实验数据均表明,其安全性分析所需的时间和空间都得到有效约减。与传统方法相比,它具有速度更快、自动化程度更高等优点。     

一种自动化模型检测ANSI-C程序的实用方法

模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术,通常的办法是手工构建一个抽象模型,然而这个方法存在一些不足,如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开发了模型提取工具C2Spin,它能够分析ANSI-C源代码,并生成对应的PROMELA验证模型,从而显著降低了建模的开销。利用C2Spin,模型检测工具SPIN可以自动地检测使用C语言编写的应用程序中的多种错误,如死锁等。在初步实验中,依靠C2Spin生成的模型,我们发现了SPIN4.3.0的一个语义错误,以及Holzmann对两个经典互斥算法的实现程序中的活锁错误。这些结果表明,C2Spin能够帮助人们更加快速有效地测试C程序。     

Software model checking is a rich research field

This introductory paper has been written for readers who know nothing about model checking but do know about software. Its aim is to present, almost without mathematical terms, the fundamental general approaches on which the papers in this Special Section build, and give an idea of what kind of contribution each paper makes. The main issues discussed are motivation for model checking, state spaces, and bounded model checking with sat solvers. Individual papers lead to discuss the following ideas: exploiting a distributed computing environment for model checking, constructing those states first that look most promising for eventually finding errors, only constructing a representative subset of states, the representation of contents of variables in an abstract way with approximation from below, and the use of more general solvers than sat solvers in bounded model checking.     

Symbolic execution with abstraction

We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously we proposed a combination of symbolic execution and model checking for the analysis of such programs: we put a bound on the size of the program inputs and/or the search depth of the model checker to limit the search state space. Here we look beyond bounded model checking and consider state matching techniques to limit the state space. We describe a method for examining whether a symbolic state that arises during symbolic execution is subsumed by another symbolic state. Since the number of symbolic states may be infinite, subsumption is not enough to ensure termination. Therefore, we also consider abstraction techniques for computing and storing abstract states during symbolic execution. Subsumption checking determines whether an abstract state is being revisited, in which case the model checker backtracks—this enables analysis of an under-approximation of the program behaviors. We illustrate the technique with abstractions for lists and arrays. We also discuss abstractions for more general data structures. The abstractions encode both the shape of the program heap and the constraints on numeric data. We have implemented the techniques in the Java PathFinder tool and we show their effectiveness on Java programs. This paper is an extended version of Anand et al. (Proceedings of SPIN, pp. 163–181, 2006).     

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

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

一种混合式内存泄漏静态检测方法

内存泄漏是导致系统性能降低的重要问题.提出一种基于模型检测算法的内存泄漏静态检查方法TMC.该方法依据程序的控制流图构建对应于程序执行的有限状态自动机,进而在此基础上应用模型检测算法分析程序中可能存在的内存泄漏.论文利用几个典型的程序实例详细说明了TMC的工作原理,并通过基于内存操作密集的测试程序集PtrDist的实验对TMC进行了验证.实验结果表明,TMC能够显著提升内存泄漏分析的精度.     

Abstract Graph Transformation

Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules.In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.