当 SOA 遇到形式化方法

你会看到人们仍然在讨论是否能成功实施SOA 。在实施SOA 的过程中，失败和成功的例子一样多。然而，成功或者失败背后的具体原因往往带有神秘色彩，这也许是因为SOA 实施人员并不知道其中的具体原因，又或是出于保密的考虑而没有公开讨论这些原因。如果实施SOA 成功了，那么最普遍的原因是该项目的治理/ 管理做得非常到位。尽管几十年的经验表明基于数学原理的系统规范和验证可以起到非常好的作用，但是我们很难听到诸如‘形式化（formal）’和‘方法（methods）’的只言片语。

早在2007 年，我们就已经讨论了W3C 在WS-CDL 上所做的工作。其中就提及到 WS-CDL 是基于 Pi 演算（Pi Calculus）的……

CDL 可以让业务干系人、业务分析师、企业架构师和应用工程师以一种同步方式分享他们关于系统的意见，其提供的方式既可以获取干系人的各类详细节，又可以使这些细节不暴露给其他人。 CDL 为各类需求提供了强有力的必要来源。通过这种方式，CDL 还确保了架构师在 SOA 中的重要地位，因为架构师决定了系统架构的建模、描述和实现。

数月后， Steve Ross-Talbot （CDL 的主要推动者之一）撰文认为“CDL 就是计算科学中的测微计”……

……在删除一行代码之前，CDL 描述不仅从需求上看是有效的，而且从计算角度（即脱离活锁、死锁和竞争条件）讲也是正确的。

Steve 又发表了一篇文章并将 CDL 的方法论称为可测试架构（Testable Architecture）。在另外一篇文章（相关视频）中，Steve 论述了几个真实案例（关于保险行业的），在这些案例中他认识到使用 WS-CDL 开发和部署 SOA 可以节省 80％的时间，实施 SOA 的成功率也有所提高。

从这两个案例可以看出，一个虚无缥缈的 SOA 路线图已经变成了现实。SOA 路线图需要整合遗留应用和门户网站，从而增强用户体验。

然后他介绍了开发这些解决方案的基于非 CDL 的初始评估：

在第一个案例中，编写解决方案和提供技术合同就用了 15 天。其中包括收集功能性和非功能性需求、制定数据模型的消息格式、理解业务处理以便解决方案能够被有效地监控，描述映射和仲裁服务间的服务契约、提供显示所需的个人服务行为的状态图以及提供协作背景的时序图。总共 4 个服务，包括客户端、仲裁、映射和遗留服务。

Steve 指出，第二个案例比较复杂，完成这些工作用了 60 天。所有的用例都用 UML 来描述，并通过可测试框架（Testable Architecture）的方法论加以验证，同时也为 CDL 模型创建了时序图，这些时序图为测试 CDL 模型提供参考。其结果非常有趣（不过从科学的角度来看，这些结果需要能够在有意义的地方进行复制。）

在第一个案例中，收集需求和创建测试模型只用了不到 1 天的时间。而在第二个案例中，完成相同的事情却用了 4 天时间。只需要点击几下鼠标就可以从 CDL 模型中生成技术性合同、WSDL、BPEL、BPMN、状态图、时序图等文件。因此可以节省 80％的时间，这或许听起来有些让人难以置信和充满神秘感。但实际上确实节省了大量时间。不仅如此，在使用 BPEL 和 WSDL 时还可以较早地发现设计缺陷。在对比需求、纠正需求和生成技术性合同方面，使用 CDL 模型比人工完成这些工作更具有严格性、完整性和明确性。

他指出，准确地描述有助于我们更好地理解我们需要什么（或认为就是需要的）。在部署之前可以验证这些描述，还可以在不影响用户的情况下彻底解决任何问题。另外，使用公认的形式化方法可以独立地开发组件，这与根深蒂固的传统观念不一样，传统观念认为只有当所有的组件部署在一起时，才能实现最初设计的功能。或正如 Steve 所说：

[我相信] 形式化方法的描述将有助于改变我们高效、高质量地完成工作的方式。因此将创建解决方案的全过程上升到了一个抽象层面，可以更好地描述解决方案。

正如上文所述，无论哪一个数据都是很难证明这件事的。但是，如果这些结果都是可复制的，它们是 SOA 架构师工具集的一个有趣的增加物。
查看英文原文： SOA Meets Formal Methods

译者简介： 陈义，计算机应用技术专业硕士研究生，一直专注于 SOA、BPM、ESB、EAI 和 MOM 的研究及应用。热衷于开源 SOA 项目，有志致力于 Mule、ServiceMix、ODE、ActiveBPEL、ActiveMQ、OpenJMS、Camel、CXF、XFire 以及 Tuscany 在中文社区的研究和推广工作。您可以通过 honnom (at) 163.com 联系到他。