基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

一种面向Web服务的拜占庭错误容忍算法

随着Web服务的高速发展,其可靠性已经受到了越来越多的重视.针对当前拜占庭错误容忍算法对Web服务支持的不足,提出并设计了一种面向Web服务的拜占庭错误容忍算法.该算法与著名的CLBFT算法有显著区别.在Web服务中,为了支持组合服务必须对进行通信的Web服务双方都创建复制品,而CLBFT算法只在服务器方创建复制品.使用基于状态机的主动复制技术,在进行通信的Web服务双方都创建复制品.引入接收窗口和接收点对异步环境下的消息进行批量确认,同步各复制品收到消息的时间.用I/O自动机给出该算法的自动机模型,并通过遵循TPC-App Benchmark规范的实验平台实现了算法,验证了算法可行性.     

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

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

基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.     

采用动作时序逻辑的Web服务组合方法

基于有限状态自动机理论,将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想。     

一种基于分层Petri网的软件工作流开发模型

软件开发模型很多,基于Web的三层结构的软件设计开发模型的关键是要考虑它的并发性.本文提出一种基于分层Petri网的Web软件开发模型.该模型对基本有限自动机进行了扩充;将扩充后的有限自动机转换成为分层状态图;根据分层状态图转换成为多功能视图;在此基础上进行软件开发.最后将这个模型发展成为分层Petri网模型,使模型更具描述能力.利用这个开发模型可以方便地进行需求分析和描述;只需开发功能子服务组件或模块,便可进行新的软件开发、系统扩充以及后来的系统重构.     

基于接口自动机的Web应用验证

Web应用的快速发展及其一些异于传统程序的特点使Web应用的验证面临了新的挑战。使用接口自动机对Web应用的构件和构件组合进行行为建模,设计了接口自动机到模型检验器Spin程序的转换算法,然后利用Spin检验Web应用的性质,通过一个简单的网上银行示例说明了整个验证过程。     

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

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

一种基于DFA的服务行为模型及其应用

本文对Web服务行为描述进行深入分析,在构造web服务自动集成结构基础上,对原有限自动机定义进行语义扩展和候选集扩展,达到准确地描述Web服务间的执行步骤、行为间简单逻辑运算关系和代价选择运算关系目的.完成服务提供商提供服务流与用户期望在该结构下的自动匹配,为web服务自动集成提供了理论依据.     

基于DTD节点自动机的XML模式验证方法

XML已经成为Web环境中数据表示和交换的标准。XML的模式验证在XML的使用中地位重要。DTD作为模式描述的一种方法,应用广泛,但使用DTD描述的模式不能正常表示同构的XML数据。文章扩展了DTD并提出了一种基于自动机的模式验证方法,将扩展的DTD中每个元素转换为一个自动机,将XML文档编码为字符串,并将字符串作为自动机的输入进行验证,可以有效地验证同构的XML。