Automatic Verification of Concurrent Ada Programs
Eric Bruneton, Jean‐François Pradat‐Peyre, Projet Sirac · 1999
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.