Reversing concurrent systems into formal specifications

Abstract

Many distributed systems are developed in traditional artistic manner. They neither have formal specifications nor the implementation are able to be reasoned or formally verified. As the number and importance of distributed systems are growing rapidly, we expect that there will be a demand of reversing these distributed systems back to formal descriptions in order to verify its correctness or to do maintenance. We discuss our experience in reversing process migration systems implemented in parallel C into CSP specifications. We reverse the program by mapping the corresponding semantic units from parallel C to CSP in step-wise reversion manner. We also discuss the problems we encountered.