Title :
Reversing concurrent systems into formal specifications
Author :
Leung, Karl R P H ; Yim, Clement F S
Author_Institution :
Dept. of Comput., Hong Kong Polytech., Kowloon, Hong Kong
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
Keywords :
C language; communicating sequential processes; formal specification; parallel languages; parallel programming; reverse engineering; CSP; CSP specifications; concurrent systems reversal; correctness; distributed systems; formal descriptions; formal specifications; parallel C; process migration systems; semantic units; step-wise reversion manner; Context; Focusing; Formal languages; Formal specifications; Message passing; Monitoring; Operating systems; Processor scheduling; Reverse engineering; Topology;
Conference_Titel :
Software Engineering Conference, 1994. Proceedings., 1994 First Asia-Pacific
Conference_Location :
Tokyo
Print_ISBN :
0-8186-6960-8
DOI :
10.1109/APSEC.1994.465257
