Volume 10, Issue 1 (2010)
MJEE 2010, 10(1): 13-38 |
Back to browse issues page
Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
Babamir S M, Jalili S. A Specification-Based Approach to Generate Verification Rules of Reactive Software. MJEE 2010; 10 (1) :13-38
URL: http://mjee.modares.ac.ir/article-17-4217-en.html
URL: http://mjee.modares.ac.ir/article-17-4217-en.html
1- University of Kashan
2- Tarbiat Modares University
2- Tarbiat Modares University
Abstract: (3368 Views)
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.
Received: 2010/11/9 | Accepted: 2010/11/9 | Published: 2010/11/9
| Rights and permissions | |
 |
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License. |