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

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

构件组合的抽象精化验证

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

一种基于抽象模板的语义Web服务组合框架

提出一个基于抽象模板的语义Web服务组合框架,并详细分析了基于该框架的抽象模板检索、数据预处理以及模板修正的实现方法.为了提高模板检索的精确度,框架采用特征匹配和图匹配相结合的方法,实现了抽象模板和用户请求之间的相似度计算.同时利用数据预处理过程构建服务之间的依赖关系图,除去了冗余的服务,并事先验证了用户请求的可满足性.根据服务依赖关系图,框架使用启发式规划修改算法(HPAA)实现了模板的自动修正,并提供了对启发式策略的灵活配置,提高了服务组合的适应性和扩展性.最后对HPAA算法中所使用的启发式策略进行了实验,验证了算法在解决大规模问题上的适应性和可靠性.     

一种基于语义消息的Web服务组合方法

在重用现有Web服务的基础上,通过服务组合形成新的、功能增值的服务是语义Web服务领域的一个重要研究内容.本文在Web服务语义描述框架的基础上,提出一种基于语义消息的Web服务组合方法,该方法定义了能够描述不同服务输出、输入消息之间对应关系的语义消息,能够业务逻辑上紧密关联的Web服务有机的组合在一起,从而为Web服务组合者以及面向服务的应用开发人员提供一种简单、直观的组合方法.     

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

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

一种基于认知模型检测的Web服务组合验证方法

近几年Web服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术,可以克服传统软件测试用例生成不完备的不足,同时具有验证自动化的优点.该文提出并实现了一种Web服务组合的认知模型检测方法,将Web服务组合建模为多主体系统,在分析BPEL语言控制流程基础上,提出BPEL活动的形式化模型,给出活动执行...     

基于概率模型检测的Web服务组合验证

Web服务组合验证对提高软件开发效率、实现服务增值具有重要意义。为了验证服务组合的有效性,提出了一种基于概率模型检测的Web服务组合验证方法。首先采用扩展的有限自动机模型建立Web服务组合模型,并将该模型转换为Markov模型,然后采用概率模型检测器PRISM验证服务组合的可靠性,最后通过实例进一步说明该方法的可行性。     

一种Web服务组合一致性验证方法研究

为解决Web服务组合事务放松ACID属性后,原子性与一致性无法保证同时满足的问题,提出了一种基于有限状态自动机的服务组合概念一致性检测方法。与以往大多通过运行时监控和协调保证应用一致性的方法不同,该方法采用有限状态自动机在设计阶段对服务组合的交互行为与异常处理进行建模,分析了概念一致性满足的关键条件和性质,证明了服务组合概念一致性的判定定理。最后通过分析服务组合一致性检测的实施框架说明了该方法的可行性。     

基于uMSD的Web服务组合验证方法研究

手工分析组合服务相当困难和耗时,为此提出了一种基于uMSD的Web服务组合的模型检验方法.如何简单和直观地表示Web服务组合的时态性质是该方法的关键问题.鉴于uMSD在简单性和表达力之间找到了一个平衡点,定义了uMSD的形式语法和语义.以Web服务组合OJA为实例,使用uMSD来图形化地表示组合服务的时态性质,展示了u...     

一种基于扩展有限自动机验证组合Web服务的方法

为简化并自动化组合Web服务验证,提出一种基于扩展有限自动机(extended deterministic finite automata,简称EDFA)验证组合Web服务的方法.使用EDFA可以准确地描述Web服务:EDFA的状态表达Web服务在与用户交互的过程中维护的状态;EDFA的状态转移及其标注描述Web服务与用户间的消息交换.EDFA给出Web服务交互过程的所有消息交换序列,刻画出Web服务的动态行为.使用基于EDFA的组合Web服务验证方法不但可以验证组合Web服务是否满足系统需求,还可以验证组合Web服务运行过程是否有逻辑错误.与其他方法相比,该方法更适于验证开放式环境下的组合Web服务.     

谓词抽象技术研究

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.     

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

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

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

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

Competent predicate abstraction in model checking

The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counterexample-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the app...     

基于抽象-验证-细化范例的软件模型检测

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测。     

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

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

Parallel Assignments in Software Model Checking

In this paper we investigate how formal software verification systems can be improved by utilising parallel assignment in weakest precondition computations.We begin with an introduction to modern software verification systems. Specifically, we review the method in which software abstractions are built using counterexample-guided abstraction refinement (CEGAR). The classical NP-complete parallel assignment problem is first posed, and then an additional restriction is added to create a special case in which the problem is tractable with an O(n²) algorithm. The parallel assignment problem is then discussed in the context of weakest precondition computations. In this special situation where statements can be assumed to execute truly concurrently, we show that any sequence of simple assignment statements without function calls can be transformed into an equivalent parallel assignment block.Results of compressing assignment statements into a parallel form with this algorithm are presented for a wide variety of software applications. The proposed algorithms were implemented in the ComFoRT reasoning framework [J. Ivers and N. Sharygina. Overview of ComFoRT: A model checking reasoning framework. Technical Report CMU/SEI-2004-TN-018, Carnegie Mellon Software Engineering Institute, 2004] and used to measure the improvement in the verification of real software systems. This improvement in time proved to be significant for many classes of software.     

Combining search space partition and search Space partition and abstraction for LTL model checking

The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size.Abstraction-based methods have been particularly successful in this regard.This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking.The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the Integration of search space partition and abstraction improves the efficiencyof verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.