摘要：在对时序逻辑语言XYZ/E进行扩展的基础上,对服务、合成服务、面向服务的体系结构以及系统的活性、正确性以及安全性等核心概念进行了形式定义,并对整个Web服务体系结构进行了形式化的描述与实现过程的分解与逐步求精,指出了在该体系结构框架下,系统的活性、正确性以及安全性存在的与服务求精过程中所具有的语义的可组合特性,这一组合特性在服务的状态转换变迁模型下得到了证明,从而为服务的合成与重用机制提供了形式化的理论指导.

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

单位：清华大学自动化系; 北京100084; 用友软件股份有限公司; 北京100085; 西安交通大学计算机科学与技术系; 陕西西安710049