Paper Info
Title
System-Level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
Abstract
The ever increasing complexity of distributed systems mandates to formally verify their design and implementation. Unfortunately, the common approaches and existing tools to formally establish the correctness of these systems remain hardly applicable to the kind of legacy applications that are commonly found in the HPC community. We present how system-level memory introspection can be achieved directly at runtime without relying on the source code analysis. We use this mechanism to detect the equality of the application's state at system level. As the storage of the system state may be memory expensive, we compact the memory by sharing unchanged memory pages between snapshots. This enables the automated verification of safety and liveness properties on legacy distributed applications written in Fortran or C/C++ using the MPI standard. We demonstrate the effectiveness of our approach on several programs from the MPICH3 test suite.
Year
DOI
Venue
2015
10.1109/PDP.2015.95
J. Log. Algebr. Meth. Program.
Keywords
Field
DocType
legacy applications
Test suite,Programming language,Source code,Computer science,Correctness,Parallel computing,Runtime verification,Verification,Legacy system,Liveness,Formal verification,Distributed computing
Conference
Volume
ISSN
Citations 
96
1066-6192
0
PageRank 
References 
Authors
0.34
28
3
Name
Order
Citations
PageRank
Marion Guthmuller100.68
Martin Quinson2132.97
Gabriel Corona300.68