基于XYZ/ADL的Web服务组合描述与验证

Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.

基于时序逻辑的软件体系结构描述语言XYZ/ADL

体系结构描述语言(architecture description language,简称ADL)是基于体系结构的软件开发的基础,便于表示求精的ADL,使得好的设计能够方便地导出好的实现.时序逻辑语言XYZ/E可在统一的逻辑框架下既表示静态语义又表示动态语义,因而基于XYZ/E的体系结构描述语言XYZ/ADL支持从高层级体系结构到低层级体系结构之间的逐步过渡.系统地阐述了XYZ/ADL的概念框架并用XYZ/E进行语义解释,介绍了如何用XYZ/ADL描述体系结构和体系结构风格.

基于XYZ/ADL的网络中心化仿真运行支撑平台体系结构形式化描述

网络中心化仿真运行支撑平台体系结构是为了满足动态构建仿真任务共同体而提出的相应支撑环境。采用基于XYZ/ADL的双重软件体系结构描述框架,分别从图形语言和形式语言对仿真运行支撑平台体系结构进行了描述并对仿真任务共同体构建中仿真核心服务层实施了分解与逐步求精。该体系结构描述方法不但从可视化角度表示了仿真运行支撑平台体系结构框图及行为抽象,还从形式化角度验证了体系结构设计的正确性和完整性。该研究是形式化描述方法在军事领域的全新尝试,为仿真运行支撑平台服务的合成与重用机制提供了形式化的理论指导。

基于XYZ/ADL的异步Web服务组合描述与验证

以Web服务组合为研究对象,重点讨论了服务组合中异步通信行为和时间属性的形式化描述和验证。首先,从软件体系结构角度分析Web服务组合,采用基于时序逻辑的XYZ/ADL描述Web服务的交互行为和时间属性;然后,提出一种符合模型检测工具UPPAAL规约的时间异步通信模型TACM;最后,实现了XYZ/RE通信命令到TACM的映射,利用UPPAAL验证了服务组合系统异步通信行为的正确性。

基于XYZ/ADL的电梯控制系统体系结构的描述与求精

研究软件体系结构的首要问题是如何描述体系结构模型;运用XYZ/ADL描述软件体系结构模型,可以在统一时序逻辑框架下描述系统静态语义到实现之间不同抽象层次的规范,便于体系结构的逐步求精及相关性质分析;以电梯控制系统为例,运用XYZ/ADL形式化地描述了系统体系结构的风格、静态模型和动态模型,并对体系结构模型的主要组件进行了逐步求精,使系统的体系结构从最初的总体功能规范平滑地过渡到了最终的可执行程序;研究表明:形式化描述语言XYZ/ADL在实时控制系统的开发中有着重要的实践意义。

基于XYZ/ADL的Web服务组合形式化描述

组合现有的Web服务是为了能快速地开发复杂的Web服务。介绍了几种常见的Web服务组合方法,并根据4种关键需求(连通性、非功能服务质量属性、正确性、可伸缩性)对它们加以比较。提出了一种基于软件体系结构描述语言XYZ/ADL的Web服务组合形式化描述方法,由XYZ/ADL定义描述Web服务的组件、组件之间交互的连接件以及建立组件和连接件实例联系的配置,最后结合一个实例描述Web服务组合的工作方式。

基于XYZ/ADL描述的选修课管理系统体系结构

XYZ/ADL是一种基于时序逻辑语言XYZ/E的可视化体系结构描述语言。文章使用XYZ/ADL对高校选修课管理系统的体系结构、客户端组件及服务器端组件进行了抽象描述,并对服务器组件中选课这一事件进行了详细描述。

基于XYZ/ADL的Web服务组合精化检验

Web服务组合的正确性验证在Web服务组合过程中至关重要.从软件体系结构角度考虑Web服务组合,可以从整体上把握系统布局.采用体系结构描述语言XYZ/ADL描述Web服务组合,并将XYZ/ADL中的XYZ/RE程序映射至时间自动机,使用精化检验方法验证Web服务组合的正确性.

体系结构描述语言XYZ/ADL到UML的映射

选择了一种基于时序逻辑语言XYZ/E的体系结构描述语言XYZ/ADL,分析了其设计元素和UML建模元素的语义,并通过UML扩展机制和对象约束语言进行扩展和约束,建立起从XYZ/ADL到UML的映射。

基于XYZ/ADL的BPEL4WS Web服务组合描述方法

Web服务组合技术作为实现面向服务体系结构的一项重要技术,已成为当今学术界和工业界共同重视的研究内容之一。基于商业流程的工业化的描述方法BPEL4WS缺乏形式化语义而无法验证描述的正确性。基于此,分析软件体系结构描述语言XYZ/ADL设计元素和BPEL4WS元素之间的语义相似性,建立XYZ/ADL至BPEL4WS的映射规则,从侧面验证BPEL4WS的正确性。

XYZ/ADL到UML的一种映射方法

分析了软件体系结构描述语言XYZ/ADL的体系结构设计元素和UML中的建模元素的语义相似性,并对UML的建模元素经过一定的扩展和约束,实现了从XYZ/ADL到UML的映射.

基于XYZ/ADL的工厂自动化系统体系结构描述与求精

XYZ/ADL是一种以时序逻辑语言XYZ/E为基础的体系结构描述语言,可同时描述软件体系结构的静态与动态行为,支持高层到低层体系结构之间的逐层过渡。本文使用XYZ/ADL描述工厂自动化系统的体系结构,采用基于组件的求精方法对主要组件进行逐步求精。

面向方面的软件体系结构描述语言AO-ADL

分析面向方面编程(AOP)的核心思想及其优越性,将编码阶段的AOP概念进一步提升到软件体系结构层次。在软件体系结构描述语言XYZ/ADL的基础上,通过增加新的元素和相关复合机制,得到一种面向方面的体系结构描述语言AO-ADL,实现了在软件体系结构中横切功能的模块化。

UML与ADL在软件体系结构建模中的应用研究

通过软件体系结构理论在实践中的应用,探讨了统一建模语言UML与体系结构描述语言ADL在软件体系结构建模中结合使用的方法和途径。着重研究了UML与XYZ/ADL在电梯控制系统体系结构建模中的应用问题,并运用基于构件的求精方法对该系统的主要组件进行了求精。

一种基于UPPAAL的Web服务组合模型检测方法

Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYZ/ADL对Web服务组合进行描述的基础上,将其实时描述部分XYZ/RE转换至时间自动机模型,组合后系统应满足的性质用分支时序逻辑CTL公式表示,最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证。

一种新型的软件体系结构描述方法研究

UML2.0与XYZ/ADL在软件体系结构描述方面具有很强的互补性,如果将两者结合起来描述软件体系结构,不仅便于开发人员之间的理解和交流,也可以对体系结构进行下一步的分析和验证。文章分析了UML2.0跟UML1.X相比在软件体系结构描述方面的改进之处,根据UML2.0与XYZ/ADL在软件体系结构描述中的对应关系,提出一种通过定义UML2.0的XYZ/E语义,将UML2.0与XYZ/ADL结合起来描述软件体系结构的一种新的途径。

一种基于体系结构的Web服务组合描述方法

Web服务组合能够快速开发复杂的Web服务,以促进Web服务的增值。在分析并比较现有的Web服务组合方法的基础上,提出了一种形式化和工业化方法相结合的Web服务组合描述方法。针对Web服务及其组合的特点,研究了基于体系结构的Web服务组合描述方法,采用扩展的XYZ/ADL定义Web服务及描述其交互的连接件,最后结合一个实例描述Web服务组合的工作方式。

UML与软件体系结构描述语言之间的转换机制研究

形式化描述和可视化描述是目前主要的两类软件体系结构描述方法,形式化描述以体系结构描述语言ADL为代表,可视化描述以统一建模语言UML为代表。目前软件体系结构描述领域的热点之一是研究这二者之间的结合,转换是其中一种重要的方式。基于此,本文对UML和基于时序逻辑的体系结构描述语言XYZ/ADL之间的转换问题进行了研究,定义了二者之间的转换规则。

面向方面的软件体系结构建模研究

分析了面向方面编程的核心思想及其概念,指出了编码阶段所存在的代码散射和缠结现象同样存在于软件体系结构中。在软件体系结构描述语言XYZ/ADL的基础上,通过增加一阶实体来表示Aspect概念,并对连接件作相应的修改,同时定义Aspect与组件之间的复合机制,提出了一种面向方面的软件体系结构建模语言AO-ADL。

基于形式化描述的电梯控制系统的建模与仿真

研究电梯控制系统中组件之间复杂的信号传输关系。针对传统的建模方法不能同时精确描述系统模型的静态与动态语义的问题,从系统体系结构的组件与连接件入手,探讨形式化描述语言XYZ/ADL描述系统模型的特性,运用XYZ/ADL形式化地描述电梯控制系统的总体功能规范、主要组件的结构模型、组件之间信号传输的动态模型和电梯运行模型,并基于所构建的形式化描述模型实现系统的仿真运行。结果表明,基于XYZ/ADL描述的形式化模型能准确分析电梯组件之间复杂的信号传输关系,精确模拟电梯运行的各种状态。