本文提出一個利用Vienna Development Method ++ (VDM++) 為正規模型以描述改善的OWL-S service model. 改善的OWL-S service model中包含改良的控制結構與敘述式。本文並包含一“BankService”的例子。本研究的好處如下：1) 使用VDM++的文法與運算子支援描述網路服務的一致性。2) 使用VDM++的staement建立服務描述的控制結構，並提供限制控制結構的方法。3) 改善的OWL-S service model可以自動的由OWL格式轉換為VDM++格式，並由VDM++的驗證工具加以驗證，故可以偵測服務描述內部的前後矛盾。 This work presents a new formal model that uses VDM++ to describe the enhanced OWL-S service model, in which additional control constructs and expressions are devised, such as selective construct and synchronization pattern. A “BankService” example is included. The benefits of this approach are: 1) VDM++ grammar and operators are used to support uniform expression of the enhanced OWL-S service model. 2) By using VDM++ statements to establish control construct of service model, control constructs with constraints are provided. 3) The enhanced OWL-S description can be automatically transformed into VDM++ specification, and verified by VDM++ verification tool. Thus, internal inconsistency in OWL description can be detected.
