In: Formal Methods and Software Engineering (ICFEM 2002), Proceedings of the 4th International Conference on Formal Engineering Methods, Shanghai, China, October 21-25, 2002, pages 262-274. Volume 2495 of Lecture Notes in Computer Science / C. George, H. Miao (Eds.) --- Springer Verlag, October 2002.
Abstract: Many approaches have been presented to detect deadlock of Ada concurrent programs. Most of them adopt some kind of flow structure or Petri nets. In this paper, we express Ada rendezvous flow structure using process algebra. Through the deduction of process algebra expressions with equivalence, information about communications among processes can be obtained. Together with the help of communication dependence analysis, the paper proposes a static approach to detect deadlock in Ada rendezvous flow structure.