Automatic verification of concurrent Ada programs

Abstract

The behavior of concurrent Ada programs is very difficult to understand because of the complexity introduced by multi-tasking. This complexity makes classical test techniques unusable and correctness can only be obtained with the help of formal methods. In this paper we present a work based on colored Petri nets formalism that automates the verification of concurrent Ada program properties. The Petri net is automatically produced by a translation step and the verification is automatically performed on the net with classical related techniques. A prototype has been developed and first results obtained allow us to think that we will be able in a near future to analyze realistic Ada programs.