基于Verics的组合Web服务有界模型检测

传统的模型检测技术无法描述系统的认知逻辑特性,而在分布式系统领域,系统和协议的规范适合用多智能体时态认知逻辑来描述.组合Web服务是典型的分布式系统.为了保证组合Web服务运行的正确性,把组合Web服务看成多智能体系统,将其建模成一组相互通信的时间自动机.采用时态认知逻辑模型检测工具Verics对该组合Web服务的可用性、可靠性和时效性的时态认知逻辑特性进行检测.本文以旅游预订系统组合Web服务为例,阐述了上述过程.     

BPEL中基于有限状态自动机的Web服务自动组合

提出了一种基于有限状态自动机的Web服务自动组合方法,该方法能够自动实现BPEL中抽象业务流程与Web服务的绑定.以有限状态自动机模型形式化地定义了业务流程的外模式和内模式,将Web服务组合问题转化为有限状态自动机问题.利用有限状态自动机的笛卡儿积运算,得出了服务组合系统的行为描述.在此基础上,提出了组合服务存在性的判定依据,进一步给出了组合服务的计算方法,设计并实现了一个演示系统.     

基于有限状态自动机的服务组合模型

分析了目前服务计算的研究现状和存在的问题，在D Berardi和A Wombacher的基础上提出了一种带条件的有限状态自动机模型cFSA（Finite State Automata with condition），并给出了基于cFSA的服务理论模型．在该服务理论模型的基础上提出了一种基于有限状态自动机的服务组合形式化模型，并给出了该模型的代数性质和实现方法．     

基于三层组织模型的一种Web服务组合策略

在研究Web服务三层组织模型和有限状态自动机的基础上,提出了一种新的Web服务组合策略,给出了一个服务的可组合性定理,并证明了定理的正确性。该策略以Web服务三层组织模型为基础,简化了BPEL中基于有限状态自动机的Web服务自动组合,精简了服务组合流程。最后对这种新的组合策略的优缺点作了分析。     

有界模型检测在服务组合中的应用研究

大规模服务自动组合问题是Web Service技术的主要瓶颈。传统的服务组合技术灵活性差并且适用的服务规模有限。在用有限状态自动描述机服务的输入、输出、操作等活动的基础上,提出用有界模型检测技术对大规模服务进行建模,将用户请求翻译为线性时态逻辑公式,采用适定性问题求解技术快速求解限定长度的服务组合解。实验结果表明有界模型检测技术应用在自动服务组合中是可行的。     

基于符号模型检测的Web服务组合形式化验证

随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求.Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题.针对此问题,提出了一种基于符号模型检测器NuSMV对Web服务组合进行验证的方法,并提出了基于消息...     

基于有限状态自动机的Web服务组合

Web服务是Web上的特殊软件资源,可以被应用系统发现和调用.如何根据用户的需求(目标服务)来组合Web服务是研究中需要解决的重要问题.通过使用有限状态自动机,服务组成的社区中的状态和操作可以使用有限状态自动机来模拟,这样可以表示服务操作的内部和外部概要.结合确定性动态命题逻辑,可以根据已有的Web服务,解决目标服务的可组合问题,产生组合计划.同时讨论了算法的复杂性.     

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

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

基于有限状态自动机的组合Web服务性能优化

组合Web服务的业务流程可以通过有限状态自动机来描述。传统的组合Web服务采用集中式的执行方式,它会带来不必要的网络流量和数据堵塞,造成大量的通信开销。提出一种基于有限状态自动机的非集中式的执行策略,在自动机的状态空间中运用启发式搜索算法执行总体代价最优的路径,从而有效减少消息传递数量,提高系统吞吐量。基于该方案设计了一个原型系统来验证系统整体性能的最优化。     

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

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

基于WSFL的Web服务组合

运用Web服务组合技术可以将越来越多的Web服务组合成一个更新更强大的服务.随着Web服务组合技术的发展,出现了各种用于描述和规范Web服务组合过程的语言.其中,WSFL是一种相对成熟的Web服务组合语言.介绍了Web服务组合的概念、方式、过程以及WSFL的相关概念,提出了使用WSFL在多个服务提供者之间进行商业过程的模型.     

基于业务规则的Web服务整合

Web服务实现了Internet环境下企业应用的松散耦合与集成,使企业可以方便地集成现有的应用和部署新的应用。当前,已有不少Web服务整合模型提出,但大多忽视了业务规则在模型中的重要作用。为此提出了一个基于结构化的业务规则的Web服务整合模型来实现业务过程的动态整合,并将详细阐述整合模型所需的基本元素和结构化业务规则思想,以及Web服务整合的过程。     

Compositional encoding for bounded model checking

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.     

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.     

Symmetry and model checking

We show how to exploit symmetry in model checking for concurrent systems containing many identical or isomorphic components. We focus in particular on those composed of many isomorphic processes. In many cases we are able to obtain significant, even exponential, savings in the complexity of model checking.The author's work was supported in part by NSF Grant CCR 941-5496, Semiconductor Research Corporation Contract 95-DP-388, and Texas Advanced Technology Program Grant 003658-250.The author's work was supported in part by NSF Grant CCR-9212183.     

基于AOP的Web服务组合容错模型

为了解决现有Web服务组合容错方案中功能性代码与容错处理代码缠绕问题,提出了基于AOP的Web服务组合容错模型.对Web服务组合执行过程的各阶段失效原因进行了分析和归类,给出了相应的容错处理策略;基于AOP横切关注点分离的思想,构建了Web服务组合容错模型,保障执行过程中业务功能和服务质量的同时,实现了容错关注点与功能关注点的分离.通过实例分析,验证了该模型的可行性和有效性.     

Bounded model checking of infinite state systems

Bounded model checking (BMC) is an attractive alternative to symbolic model checking, since it often allows a more efficient verification. The idea of BMC is to reduce the model checking problem to a satisfiability problem of the underlying base logic, so that sophisticated decision procedures can be utilized to check the resulting formula. We present a new approach to BMC that extends current methods in three ways: First, instead of a reduction to propositional logic which restricts BMC to finite state systems, we focus on infinite state systems and therefore consider more powerful, yet decidable base logics. Second, instead of directly unwinding temporal logic formulas, we use special translations to ω-automata that take into account the temporal logic hierarchy and maintain safety and liveness properties. Third, we employ both global and local model checking procedures to take advantage of the different types of specifications that can be handled by these techniques. Based on three-valued logic, our bounded model checking procedures may either prove or disprove a specification, or they may explicitly state that no information has been obtained due to insufficient bounds.