基于XYZ/ADL的Web服务体系结构形式描述  

XYZ/ADL Based Web Services Architecture Description

作　　者：饶元[1] 李尊朝[2] 

机构地区：[1]清华大学自动化系 [2]西安交通大学计算机科学与技术系,陕西西安710049

出　　处：《系统工程理论与实践》2006年第3期53-60,共8页Systems Engineering-Theory & Practice

基　　金：国家863高技术研究发展计划(2003AA4Z3230;2005AA4Z3210);西安市科技计划项目(KS200306)

摘　　要：在对时序逻辑语言XYZ/E进行扩展的基础上,对服务、合成服务、面向服务的体系结构以及系统的活性、正确性以及安全性等核心概念进行了形式定义,并对整个Web服务体系结构进行了形式化的描述与实现过程的分解与逐步求精,指出了在该体系结构框架下,系统的活性、正确性以及安全性存在的与服务求精过程中所具有的语义的可组合特性,这一组合特性在服务的状态转换变迁模型下得到了证明,从而为服务的合成与重用机制提供了形式化的理论指导.With the progress of web service rcsue and composition technology, how to guarantee the verification of service teachability, liveness and correctness in the process of service deployment and state transition has become a bottleneck to influence further development about web service-based applications. The formal definitions about service, compositional service and service-oriented architecture as well as the teachability, the liveness, the correctness of system are defined under the basis of the extended emperal logical language XYZ/E. The whole web services architecture was decomposed and the stepwise refinement process was formally described for concretely realization by refinement programming. Furthermore, the property of semantic composition about liveness, correctness and security of system in the process of service refinement has been proven by service statement transition model （SSTM） and XYZ/ ADL language, which provided a formally theoretical instruction for service reuse and composition.

关 键 词：WEB服务 软件体系结构 WEB服务合成 时序逻辑 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]