رویکردی مبتنی بر توصیف برای تولید قوانین درستی یابی نرم افزار های واکنشی

از آنجا که رویکردهای درستی یابی ایستا1 و آزمون نرم افزار، برای اطمینان یافتن از درستی عملکرد نرم افزار ها کافی نیست، رویکرد دیگری به نام درستی یابی در زمان اجرا2 - که در آن درستی نرم افزار در برابر قیود3 در زمان اجرای واقعی نرم افزار انجام می شود - مورد استقبال قرار گرفته است. اما مشکلی که این رویکرد با آن روبه رو است، درستی یابی فعالیت های زمان اجرای نرم افزار در برابر توصیف های انتزاعی4 و سطح بالای قیود است زیرا ماهیت فعالیت های زمان اجرا و توصیف های انتزاعی با یکدیگر متفاوت است. در این مقاله با تکیه بر نرم افزار های واکنشی5، رویکردی به نام SRG6 ارائه می شود که در طی سه مرحله، از روی توصیف های انتزاعی مساله و قیود، به تولید خودکار قوانین حقیقی - که برحسب کمیت های فعالیت های زمان اجرا بیان می شود –می پردازد تا درستی یابی رفتار اجرایی نرم افزار را ممکن سازد. در این رویکرد: (1) یک مدل بصری واکنشی از توصیف مساله ارائه شده و سپس، ضوابط رفتار حین اجرای نرم افزار برحسب منطق بی درنگ7 تولید می شود، (2) قیودی که باید در زمان اجرا به وسیله نرم افزار رعایت شوند برحسب منطق بی درنگ توصیف می شود و (3) قوانین درستی یابی از قیود (مورد 2) برحسب ضوابط رفتار نرم افزار (مورد 1) تولید می شود. در پایان رویکرد SRG را برای مساله “پروتکل ارتباطات پیامی” به کار می بریم.