论文部分内容阅读
随着业务过程的结构及交互过程越来越复杂，设计出的系统需要数次的模型转换——由较抽象的纯业务过程模型转换为较低层次的可执行的应用型模型，如BPEL4WS。但在这些模型的转换结束之后，一些关键的特性必须能被维持。为了确保这些特性在模型转换后仍然能够成立，本文通过将BPEL4WS转换为Promela语言而将模型需要维持的特性转换为线性时态逻辑的表达式。从而使用模型检测工具Spin来验证BPEL4WS是否对抽象的业务过程模型设计中所要求的重要特性保持了一致性。