افسون سلطانی - دانشجوی کارشناسی ارشد، گروه کامپیوتر،دانشگاه آزاد اسلامی واحد اراک

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

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