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

از آنجا که رويکردهاي درستي يابي ايستا و آزمون نرم افزار، براي اطمينان يافتن از درستي عملکرد نرم افزار ها کافي نيست، رويکرد ديگري به نام درستي يابي در زمان اجرا - که در آن درستي نرم افزار در برابر قيود در زمان اجراي واقعي نرم افزار انجام مي شود - مورد استقبال قرار گرفته است. اما مشکلي که اين رويکرد با آن روبه رو است، درستي يابي فعاليت هاي زمان اجراي نرم افزار در برابر توصيف هاي انتزاعي و سطح بالاي قيود است زيرا ماهيت فعاليت هاي زمان اجرا و توصيف هاي انتزاعي با يکديگر متفاوت است. در اين مقاله با تکيه بر نرم افزار هاي واکنشي، رويکردي به نام SRG⁶ ارايه مي شود که در طي سه مرحله، از روي توصيف هاي انتزاعي مساله و قيود، به توليد خودکار قوانين حقيقي - که برحسب كميت هاي فعاليت هاي زمان اجرا بيان مي شود-مي پردازد تا درستي يابي رفتار اجرايي نرم افزار را ممکن سازد. در اين رويکرد: (1) يک مدل بصري واکنشي از توصيف مساله ارايه شده و سپس، ضوابط رفتار حين اجراي نرم افزار برحسب منطق بي درنگ توليد مي شود، (2) قيودي که بايد در زمان اجرا به وسيله نرم افزار رعايت شوند برحسب منطق بي درنگ توصيف مي شود و (3) قوانين درستي يابي از قيود (مورد 2) برحسب ضوابط رفتار نرم افزار (مورد 1) توليد مي شود. در پايان رويکرد SRG را براي مساله «پروتكل ارتباطات پيامي» به کار مي بريم.