Hide/Show Apps

Scalable Software Model Checking Using Design for Verification

2005-11-13
TEVFİK, Bultan
Betin Can, Aysu
Show full item record
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
2
views
0
downloads
There has been significant progress in automated verification techniques based on model checking. However, scalable software model checking remains a challenging problem. We believe that this problem can be addressed using a design for verification approach based on design patterns that facilitate scalable automated verification. We have been investigating a design for verification approach based on the following principles: 1) use of stateful, behavioral interfaces which isolate the behavior and enable modular verification, 2) an assume-guarantee style verification strategy which separates verification of the behavior from the verification of the conformance to the interface specifications, 3) a general model checking technique for interface verification, and 4) domain specific and specialized verification techniques for behavior verification. So far we have applied this approach to verification of synchronization operations in concurrent programs and to verification of interactions among multiple peers in composite web services. The case studies we conducted indicate that scalable software verification is achievable in these application domains using our design for verification approach
Computer science, software engineering, Computer science, theory and methods
https://hdl.handle.net/11511/56061
Graduate School of Informatics, Conference / Seminar
METU IIS - Integrated Information Service IT Support Service
You can transmit your request, problems about services
provided by METU Computer Center, and follow the process.