In: Proc. 3-rd Int. IEEE High-Assurance Systems Engineering Symposium, 13-14 November 1998, Washington, DC, pages 124-133. 1998.
Abstract: This paper deals with verification of flow control in concurrent programs. Ada language is used as a reference. After translation of Ada programs into Petri nets (named Ada nets for Ada programs), it is shown how one can fully exploit the relationship between the behavior of the concurrent program and the structure of the corresponding Petri net. Using the siphon structure, some structural conditions are refined for behavioral properties such as liveness and deadlock-freeness that correct concurrent programs must satisfy. These conditions can be proved or disproved using efficient algorithms. A formal justification of guidelines (such as client/server paradigm) that programmers observe traditionally in order to build correct concurrent programs is also provided. Several examples are presented to show the effectiveness of using structure theory of Petri nets for static analysis of concurrent programs.
Keywords: Petri nets, concurrent programming, program verification, structural methods.