Tarbiat Modares University The Modares Journal of Electrical Engineering 2228-527X 10 1 2010 04 01 A Specification-Based Approach to Generate Verification Rules of Reactive Software رویکردی مبتنی بر توصیف برای تولید قوانین درستی‌یابی نرم‌افزار‌‌های واکنشی 13 38 12882 EN Seyed Morteza Babamir University of Kashan Sayed Jalili Tarbiat Modares University Journal Article Static verification and software testing are not able to verify software single-handedly. Therefore, another approach called run-time verification dealing with verifying software behavior against constraints at run-time received attention. However, the run-time verification faces the problem of verification of run-time activities against the constraints are specified in high-level and abstractly because their natures are different from each other. Focused on reactive software, in three steps this paper presents an approach called SRG to generate run-time verification rules in terms of run-time activities from abstract specification and constraints of problem. The approach: (1) presents a visual and reactive model of problem specification and then generates ground rules of run-time behavior of software in real-time logic, (2) specifies in real-time logic the constraints should be met by software at run-time, and (3) generates verification rules from the constraints and the ground rules. Last of all, the SRG approach is applied to message communication protocol. https://mjee.modares.ac.ir/article_12882_71964ed9f684f669180eed60be305c42.pdf