【作者】 苏焕程； 黄志球； 刘林源；

【Author】 SU Huan-cheng HUANG Zhi-qiu LIU Lin-yuan College of Information Science & Technology,Nanjing University of Aeronautics & Astronautics 210016

【机构】 南京航空航天大学信息科学与技术学院；

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

【Abstract】 As the organization and interaction in Business Processs are becoming more and more complicated,it usually needs multiple translations from the initial business model downward to the application model,such as BPEL4WS.There are some key requirements must be held during the translations.In order to make sure the key requirements won’t be missed in each model,this paper verify whether the BPEL4WS are consistent to Business Process Model based on Spin by translates BPEL4WS to Promela and translates re- quirements to Linear Temporal Logic.更多还原