● 摘要
面向服务架构（SOA）代表了软件开发的最新发展方向，它的成熟与发展将引领软件行业的新一轮发展高潮。SOA的核心思想是以服务为基本单位，通过服务重用和快速组合构建随需应变的松耦合分布式应用系统。目前，基于Web服务的应用程序功能越来越强大、越复杂，给设计与构建健壮的Web服务软件带来了挑战。本文探索了一种在软件设计阶段对软件进行测试的方法，即采用形式化方法对软件系统体系结构和需求特性进行描述得到形式化模型，再采用形式化工具对该模型进行形式化验证，分析软件系统的内在性质，从而在软件设计阶段检测出软件中出现的与软件需求特性不符的错误。通过修正这些错误有助于减少软件实现后期的测试工作量和测试强度，从而降低软件开发成本，提高软件质量。为了使用形式化方法对软件进行描述和验证，本文提出了一种基于重写逻辑的形式化建模和形式化验证方案：使用OWL-S描述软件体系结构，以重写逻辑支持其中的动态语义（模型转换），得到形式化模型，然后对该形式化模型进行基于重写逻辑的形式化验证。本文的主要工作内容包括：(1)提出了一种将OWL-S模型转换为Maude模型的方法，并在此基础上设计、实现了自动转换工具。以OWL-S重写框架为基础，研究了具体的模型从OWL-S语言向Maude语言转换的方法。该方法对OWL-S模型的IOPE、数据绑定、控制结构和进程主体等各个组成部分以及涉及的数据类型分别进行转换，并为进程构建一个执行环境作为形式化验证的初始状态，通过整合这些转换生成完整的Maude模型。(2)采用Maude系统提供的形式化验证工具对转换得到的Maude模型进行了形式化验证。形式化验证包括非功能属性验证和功能属性验证两部分，非功能属性验证指验证转换得到的Maude模型是否满足与系统功能无关的属性，如终止性、合流性、完备性和一致性；功能属性验证即验证使用Maude语言描述的软件系统是否满足软件的需求特性，从而检测软件在设计方面不满足软件需求特性的错误。(3)在上述内容的基础上，设计、实现了一个集成OWL-S模型转换与形式化验证功能的OWL-S模型转换与形式化验证原型系统。同时使用OWL-S构建相应的Web服务软件实例，应用本文所实现的原型系统针对实例进行模型转换与形式化验证，通过分析结果验证本文所述方法及原型系统的有效性。