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

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

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