Sciweavers

SIGSOFT
2004
ACM

Automating comprehensive safety analysis of concurrent programs using verisoft and TXL

13 years 11 months ago
Automating comprehensive safety analysis of concurrent programs using verisoft and TXL
In run-time safety analysis the executions of a concurrent program are monitored and analyzed with respect to safety properties. Similar to testing, run-time analysis is quite efficient, but it also tends to be incomplete. The results pertain only to the observed executions which may constitute just a small subset of all possible executions. In this paper, we describe a tool called ViP which uses the software model checker VeriSoft to perform comprehensive run-time safety analyses of concurrent C/C++ programs. A ViP analysis proceeds in three fully automated steps: First, the input program is prepared for a VeriSoft analysis through instrumentation. Next, VeriSoft is invoked to generate the traces corresponding to all possible executions of the program. Then, the traces are checked efficiently for specification violations. The instrumentation is based on the source code transformation language TXL. TXL allows for the instrumentation to be described in terms of rewrite rules and gives...
Jürgen Dingel, Hongzhi Liang
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where SIGSOFT
Authors Jürgen Dingel, Hongzhi Liang
Comments (0)