基于SPIN的BPEL4WS一致性验证
随着业务过程的结构及交互过程越来越复杂，设计出的系统需要数次的模型转换——由较抽象的纯业务过程模型转换为较低层次的可执行的应用型模型，如BPEL4WS。但在这些模型的转换结束之后，一些关键的特性必须能被维持。为了确保这些特性在模型转换后仍然能够成立，本文通过将BPEL4WS转换为Promela语言而将模型需要维持的特性转换为线性时态逻辑的表达式。从而使用模型检测工具Spin来验证BPEL4WS是否对抽象的业务过程模型设计中所要求的重要特性保持了一致性。
业务过程 业务过程执行语言 线性时态逻辑 一致性验证 模型转换 模型设计
苏焕程 黄志球 刘林源
南京航空航天大学信息科学与技术学院 210016
国内会议
山东烟台
中文
102-106
2008-10-31（万方平台首次上网日期，不代表论文的发表时间）