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...

• Type: Conference
• Year: 2004
• Where: SIGSOFT
• Authors: Jürgen Dingel, Hongzhi Liang
• Keywords: Possible Executions, Run-time Safety, Run-time Safety Analysis, SIGSOFT 2004, Software Engineering