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

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

基于MAS模型检测与抽象的Web服务验证

Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统( MAS)模型检测工具( MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。     

基于CEGAR的Web应用验证

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.     

构件组合的抽象精化验证

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.     

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

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

反例引导的模型检验工具的设计

针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.     

变量极小不可满足在模型检测中的应用

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.     

结构化组合补偿抽象精化性质研究

为解决松耦合Web事务复杂业务流程的建模问题,确保组合事务的可靠性和一致性,提出一种基于配对Petri网的结构化组合补偿精化方法,实现复杂多伙伴业务流程的抽象层次建模.定义了4种基于配对Petri网的基本组合补偿结构:顺序、并行、选择和循环结构.引入组合流程精化和组合补偿抽象的定义,分析了复杂业务流程的精化和抽象过程,给出了精化流程应满足的性质.通过具体业务实例验证了该精化和抽象方法的可行性.     

嵌入式PLC中顺序功能图向AOV的映射

为实现PLC顺序功能图语言向梯形图语言的转换,阐述了将PLC的顺序功能图映射为有向图的思想与实现算法.首先对顺序功能图图形网络的描述方式进行严格定义,提出了一种新的AOV节点定义,把顺序功能图中的步元件与其前后连接信息相结合抽象为AOV图的顶点,步元件之间的转换关系抽象为弧,然后在此基础上提出了统一的顺序功能图程序结构的表达方式.本算法在保持顺序功能图结构完整性的基础上,简化了模型,同时可以很好地检查其中的连接错误,为从图的角度研究顺序功能图向梯形图的转化打下了基础.基于本算法思想设计的可编程逻辑控制器编程平台也在实际应用中得到验证,进一步证明其正确性和可用性.     

基于活性顺序图的形式化验证方法及工具研究

近年来,形式化验证方法在软件开发过程的作用越来越大;如何充分利用形式化验证方法提高软件系统的可靠性已成为软件开发者及使用者主要关注的问题;总结了近年来基于活性顺序图的形式化验证方法的研究进展,首先介绍活性顺序图的语言及其表达能力与复杂性,然后深入分析现有的基于活性顺序图的形式化验证的关键技术及其典型应用,最后实现一种基于活性顺序图的运行时验证工具,实验证明使用本验证工具进行形式化验证的可行性。     

Counterexample-guided abstraction refinement for linear programs with arrays

Predicate abstraction refinement is one of the leading approaches to software verification. The key idea is to abstract the input program into a Boolean Program (i.e. a program whose variables range over the Boolean values only and model the truth values of predicates corresponding to properties of the program state), and refinement searches for new predicates in order to build a new, more refined abstraction. Thus Boolean programs are commonly employed as a simple, yet useful abstraction. However, the effectiveness of predicate abstraction refinement on programs that involve a tight interplay between data-flow and control-flow is still to be ascertained. We present a novel counterexample guided abstraction refinement procedure for Linear Programs with arrays, a fragment of the C programming language where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. In our procedure the input program is abstracted w.r.t. a family of sets of array indices, the abstraction is a Linear Program (without arrays), and refinement searches for new array indices. We use Linear Programs as the target of the abstraction (instead of Boolean programs) as they allow to express complex correlations between data and control. Thus, unlike the approaches based on predicate abstraction, our approach treats arrays precisely. This is an important feature as arrays are ubiquitous in programming. We provide a precise account of the abstraction, Model Checking, and refinement processes, discuss their implementation in the EUREKA tool, and present a detailed analysis of the experimental results confirming the effectiveness of our approach on a number of programs of interest.     

基于Event-B 方法的多应用智能卡的建模与开发

Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成。该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性。为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event-B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用。     

Model checking unbounded concurrent lists

We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification community. These data structures are unbounded in two dimensions: the list size is unbounded and an unbounded number of threads access them. Thus, their model checking requires abstraction to a model bounded in both the dimensions. We first show how the unbounded number of threads can be model checked by reduction to a finite model, while assuming a bounded number of list nodes. In particular, we leverage the CMP (CoMPositional) method which abstracts the unbounded threads by keeping one thread as is (concrete) and abstracting all the other threads to a single environment thread. Next, the method proceeds as a series of iterations where in each iteration the abstraction is model checked and, if a spurious counterexample is observed, refined. This is accomplished by the user by inspecting the returned counterexamples. If the user determines the returned counterexample to be spurious, she adds constraints to the abstraction in the form of lemmas to refine it. Upon addition, these lemmas are also verified for correctness as part of the CMP method. Thus, since these lemmas are verified as well, we show how some of the lemmas required for refinement of this abstract model can be mined automatically using an assertion mining tool, Daikon. Next, we show how the CMP method approach can be extended to the list dimension as well, to fully verify the data structures in both the dimensions. While it is possible to show correctness of these data structures for an unbounded number of threads by keeping one concrete thread and abstracting others, this is not directly possible in the list dimension as the nodes pointed to by the threads change during list traversal. Our method addresses this challenge by constructing an abstraction for which the concrete nodes, i.e., the nodes pointed to by the threads, can change as the thread pointers move with program execution. Further, our method also allows for refinement of this abstraction to prove properties of interest. We show the soundness of our method and establish its utility by model checking challenging concurrent list-based data structure examples.     

Blaming the client: on data refinement in the presence of pointers

Data refinement is a common approach to reasoning about programs, based on establishing that a concrete program indeed satisfies all the required properties imposed by an intended abstract pattern. Reasoning about programs in this setting becomes complex when use of pointers is assumed and, moreover, a well-known method for proving data refinement, namely the forward simulation method, becomes unsound in presence of pointers. The reason for unsoundness is the failure of the “lifting theorem” for simulations: that a simulation between abstract and concrete modules can be lifted to all client programs. The result is that simulation does not imply that a concrete can replace an abstract module in all contexts. Our diagnosis of this problem is that unsoundness is due to interference from the client programs. Rather than blame a module for the unsoundness of lifting simulations, our analysis places the blame on the client programs which cause the interference: when interference is not present, soundness is recovered. Technically, we present a novel instrumented semantics which is capable of detecting interference between a module and its client. With use of special simulation relations, namely growing relations, and interpreting the simulation method using the instrumented semantics, we obtain a lifting theorem. We then show situations under which simulation does indeed imply refinement.     

Relational concurrent refinement part III: traces,partial relations and automata

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.     

Calculating upward and downward simulations of state-based specifications

This paper concerns calculational methods of refinement in state-based specification languages. Data refinement is a well-established technique for transforming specifications of abstract data types into ones, which are closer to an eventual implementation. The conditions under which a transformation is a correct refinement are encapsulated into two simulation rules: downward and upward simulations.One approach for refining an abstract system is to specify the concrete data type, and then attempt to verify that it is a valid refinement of the abstract type. An alternative approach is to calculate the concrete specification based upon the abstract specification and a retrieve relation, which links the abstract and concrete states. In this paper we generalise existing calculational methods for downward simulations and derive similar results for upward simulations; we also document their use and application in a particular specification language, namely Z.     

一种基于近似因子的在线概率知识库推理方法

概率知识库中的推理技术是近年来的研究热点。目前大多数系统的推理主要基于批处理的方式实现,并不适用于在线查询场景。针对此本文提出了一种基于近似因子的在线概率知识库推理方法,它可重复利用已推断结果计算查询变量的边缘概率。该算法首先提取查询变量的子图（含已推断变量）;接着在此子图上添加近似因子以模拟子图外其余变量的影响;最后采用团树算法推断查询变量的边缘概率。实验结果表明,相较于已有算法,本文算法可在时间和精度上取得较好的权衡。.     

形式化方法B的精化

形式化方法B支持从抽象规约到实现的完整的开发过程，用于开发安全关键的软件系统。给出了B方法精化的定义后，介绍了抽象机的精化过程与方法，结合实例分析了仅使用前向精化的普通精化规则的不完整性，通过引入反向精化提供了完备的精化理论，二者联合起来能够证明任何正确的精化。     

Lazy Slicing for State-Space Exploration

CEGAR (Counterexample-guided abstraction refinement)-based slicing is one of the most important techniques in reducing the state space in model checking.However,CEGAR-based slicing repeatedly explores the state space handled previously in case a spurious counterexample is found.Inspired by lazy abstraction,we introduce the concept of lazy slicing which eliminates this repeated computation.Lazy slicing is done on-the-fly,and only up to the precision necessary to rule out spurious counterexamples.It identifies a spurious counterexample by concretizing a path fragment other than the full path,which reduces the cost of spurious counterexample decision significantly.Besides,we present an improved over-approximate slicing method to build a more precise slice model.We also provide the proof of the correctness and the termination of lazy slicing,and implement a prototype model checker to verify safety property.Experimental results show that lazy slicing scales to larger systems than CEGAR-based slicing methods.