OWL-S在描述Composite Process的时候提供了顺序、分支等控制结构，我想利用这些控制结构来描述基于Web服务的软件系统的组成结构，即把整个软件系统看作一个Composite Process。

这算不算是一种形式化的表示方法呢？

看大家以前的帖子，觉得形式化方法总要和一种经典理论有关，如Petri网、时态逻辑、Pi演算、进程代数等，我因此很困惑，不知道这种采用OWL-S来描述系统结构的方法算不算是形式化的表示方法呢？一定要和一种经典理论挂钩吗？

而是采用OWL-S来描述系统结构的方法不容易操作呀
---我大致的设想是象OWL-S Editor中对Composite Process的处理那样，以图形化的方式来描述系统的结构，数据的存储方式为OWL-S。在对OWL-S不能满足描述系统需要的地方进行扩充。（并不为了丰富OWL-S，只是扩充后能够满足具体应用的需要就行了。）

我刚看了这篇文章：
《基于Pi-演算的Web服务组合的描述和验证》，廖军，计算机学报，2005，28（4）

文中的结论部分提到：

“许多现有的Web服务及其组合描述语言都是半形式化的，容易出错且不易检测和验证，也没有相应形式化工具的支持，这使得Web服务组合的正确性难以保证，其流程也无法在较抽象的层次上跟踪。在这种背景下，出现了许多形式化方法，如基于Petri网、进程代数的方法。”

这是不是解答了我对于OWL-S是否属于形式化方法的困惑呢？它是否只属于半形式化方法？
要对它进行推理和验证，需要把它转化成别的形式化方法，然后再用对应的形式化工具支持推理和验证吗？

这也是在有了BEPEL4WS、OWL-S等描述语言之后，大家还再采用Petri网、进程代数等方法进行分析验证的原因吗？即它们都只是半形式化的方法。

我对这些描述语言与这些形式化方法的关系实在搞不清，请大家多指教！

基于OWL-S的动态服务组合和基于petri net、进程代数等的静态服务组合是两个不同的流派。

基于OWL-S的动态服务组合和基于petri net、进程代数等的静态服务组合是两个不同的流派。

不胜感激