[BP99] Automatic Verification of Concurrent Ada Programs

Conférence Internationale avec comité de lecture : Ada-Europe99, , January 1999,
Résumé: 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.


@inproceedings {
title="{Automatic Verification of Concurrent Ada Programs}",
author=" E. Bruneton and J. Pradat-Peyre ",
booktitle="{Ada-Europe99, }",