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