Capturing and Verifying Dynamic Program Behaviour Using UML Communication Diagrams and Pi-Calculus

UML is a semi-formal modeling language for object oriented systems. It is successfully used to assist all phases of software development process. With growing support by CASE tools, its applications become more and more widespread in real word projects. In fact, these tools allow code-generation from UML diagrams and reverse-engineering. In other hand, picalculus is a flexible formal theory with several applications especially for distributed systems. It offers a rich theory and tools for verification purposes. Thus, this paper presents an approach for capturing and verifying the dynamic behavior of programs using UML communication diagrams (collaboration diagrams in UML 1.x) and pi-calculus. We illustrate our approach by an example in order to explain the general purpose usability of our approach. Then we tackle another small example to show the verification capabilities provided by the approach.