一种支持网上服务组合的形式化验证
目前，面向服务架构(SOA)成为现代企业应用的最受青睐的软件架构，而其实现的一个重要技术就是Web服务。Web服务是一种能够通过Web发布、查找、调用的自包含、自描述、模块化的应用。随着越来越多的Web服务的出现，在不同的Web服务之间共享信息就显得很重要。由于服务组合的复杂性，保证服务组合的正确性是十分必要的。形式化方法对于Web服务组合的描述及验证，有效地保证了服务组合的正确性。本文对Web服务、Web服务的体系结构以及Web服务组合进行介绍。在此基础上，为确保Web服务组合的正确性和可靠性，引入了形式化的方法，运用形式化方法对Web服务组合进行描述，并在此描述基础上进行验证。最后给出一个典型的订票服务，运用CCS对其进行描述，借助其支持工具CWB对CCS模型进行验证。下一步工作是，服务描述与代数描述间的双向转换，以及基于形式化方法的自动代码生成。
服务组合 形式化方法 形式化验证 面向服务架构 软件架构 订票服务 代码生成
云本胜 严隽薇 刘敏
同济大学CJMS研究中心
国内会议
上海
中文
97-101
2007-07-28（万方平台首次上网日期，不代表论文的发表时间）