چكيده
مدلهاي گردش كار در زمينه هاي متنوعي داراي كاربرد بوده و درستي يابي و بررسي مدل آنها داراي اهميت فراواني است . روشهاي مختلفي براي مدلسازي سيستمهاي گردش كار معرفي شده است . كه از مهمترين آنها مي توان به شبكه هاي گردش كار YAWL ,BPEL اشاره كرد . يكي از اهداف مدلسازي سيستمهاي گردش كار تحليل آنها با روش بررسي مدل است . اين پايان نامه بر بررسي مدل سيستمهاي گردش كار ،كه با استفاده از شبكه هاي گردش كار ( كه نوع خاصي از شبكه هاي پتري هستند ) يا زبان اجرايي فرايند تجاري مدلسازي شده اند متمركز است . براي بررسي مدل ايجاد شده از ابزار باگر استفاده خواهد شد . استفاده از اين ابزار جديد و پرقدرت مي تواند بررسي اين مدلها را تسهيل نموده و براي طراحي سيستم هاي گردش كار كه درست و معتبر باشند كمك نمايد . ابزار باگر مبتني بر زبان جاوا بوده و متن باز است . به منظور فراهم سازي امكان بررسي مدلهاي گردش كار با اين ابزار لازم است كه مدلهاي گردش كار با استفاده از يك مبدل به ورودي ابزار باگر كه زبان BIR است تبديل شوند . كار اصلي انجام شده در اين پايان نامه ارائه يك چارچوب كامل براي مدلسازي و درستي يابي سيستمهاي گردش كار است . همچنين براي نشان دادن اثر بخش بودن چارچوب پيشنهادي ،مطالعات موردي متعددي انجام شده است . تبديل مدلهاي گردش كار و همچنين مقايسه باگر با ديگر بررسي كننده ها ، از جمله كارهاي انجام شده در اين پايان نامه محسوب مي شوند .
