Web Service Choreography Verification Using Z Formal Specification
محل انتشار: ماهنامه بین المللی مهندسی، دوره: 29، شماره: 11
سال انتشار: 1395
نوع سند: مقاله ژورنالی
زبان: انگلیسی
مشاهده: 412
فایل این مقاله در 9 صفحه با فرمت PDF قابل دریافت می باشد
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
JR_IJE-29-11_008
تاریخ نمایه سازی: 9 خرداد 1396
چکیده مقاله:
Web Service Choreography Description Language (WS-CDL) describes and orchestrates the services interactions among multiple participants. WS-CDL verification is essential since the interactions would lead to mismatches. Existing works verify the messages ordering, the flow of messages, and the expected results from collaborations. In this paper, we present a Z specification of WS-CDL. Besides verifying the mentioned concerns, we find out whether the choreographies are realizable by web services protocols at orchestration level. In this regard we detect the interactions between each two distinct participants which lead to deadlock or unspecified reception. An „itinerary purchase‟ case study for prototyping the transformation rules is presented and the Z/EVES tool is used to demonstrate the protocol compatibility. Also, we define multiple attributes to compare the choreography description languages/models from the verification and adaptation viewpoints
کلیدواژه ها:
نویسندگان
y Rastegari
Department of Computer Science and Engineering, Shahid Beheshti University, Tehran, Iran
z Sajadi
Department of Computer Science and Engineering, Shahid Beheshti University, Tehran, Iran
f shams
Department of Computer Science and Engineering, Shahid Beheshti University, Tehran, Iran