ارائه یک روش صوری برای مدلسازی و راستی آزمایی سیستم های گردش کار زمانی

هدف اصلی سیستم های مدیریت گردش، پشتیبانی از تعریف، اجرا و کنترل فرایندهای کسب و کار است . در چنین سیستم هایی خطاها در مشخصه ها باید به زودی ممکن شناسایی و اصلاح شوند. از طرفی ترکیب محدودیت های زمانی مسئله را وخیم تر می کنند. در حالی که سیستم های گردش کار موجود پشتیبانی محدودی از مسائل زمانی ارائه می دهند. از طرفی، پیاده سازی مدل های گردش کار بزرگ و راستی آزمایی نشده در خطر زمان اجرای نامطلوب قرار دارند. استفاده از روش های صوری برای خودکارسازی راستی آزمایی ها ضروری به نظر می رسد، اما به خاطر پیچیدگی آن کمتر مورد توجه قرار گرفته است. لذا رهیافت موجود با هدف غنی نمودن گردش کار با محدودیت های زمانیف مدلسازی را با مفهوم صوری آتاماتای زمانی ترکیب می کند. این رهیافت برای راستی آزمایی، ابزار بلادرنگ UPPAAL را به کار می گیرد.

کلیدواژه ها:

گردش کار ، راستی آزمایی ، روش صوری ، مدلسازی ، آتاماتای زمانی