Abstract: In order to solve the problem of composition and verification of semantic Web services，this paper proposes a composite method based on Model-Driven Architecture（MDA） and a matching method based on semantic matching degree.In the static aspects，the OWL-S is modeled by the composite method using UML class diagrams and use-case diagram.The dynamic composition of OWL-S is modeled by the use of activity diagram.In the procedure of modeling，a matching method based on semantic matching degree is used to choose a subset of Web services for determining the most appropriate composite Web service and the compositing UML model is translated into the verifiable Promela language by the model checking tools，SPIN.The verified UML model，as a template，is stored in ontology knowledge base.The model improves the efficiency of the semantic Web services，and ensures the process of dynamic composition accuracy.By the use of templates and semantic matching degree，the most suitable and available Web services can be found and selected.

Key words: semantic Web service, composite verifying model, Model Driven Architecture（MDA）, semantic matching degree

摘要： 针对语义Web服务的组合与验证问题，提出了基于模型驱动架构（MDA）的组合方法与基于语义匹配度的匹配方法。组合方法使用UML类图和用例图对OWL-S进行静态组合建模，使用活动图对OWL-S进行动态组合建模。在建模过程中使用基于语义匹配度的匹配方法，选择可用的子Web服务确定最合适的组合Web服务，并将该组合UML模型转化为可验证的Promela语言，使用SPIN工具进行验证，通过验证的UML模型作为模板保存于本体的知识库中以便使用。该模型提高了开发语义Web服务的效率，保证了组合过程的正确性，还能利用模板与语义匹配度实时发现与选择可用的Web服务。

关键词: 语义Web服务, 组合验证模型, 模型驱动架构（MDA）, 语义匹配度