|
 
|
[BP99] Automatic Verification of Concurrent Ada Programs
Conférence Internationale avec comité de lecture : Ada-Europe’99, , January 1999,
motcle:
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.
BibTeX
| @inproceedings { | |||
| BP99, | |||
| title | = | "{Automatic Verification of Concurrent Ada Programs}", | |
| author | = | " E. Bruneton and J. Pradat-Peyre ", | |
| booktitle | = | "{Ada-Europe’99, }", | |
| year | = | 1999, | |
| month | = | "January", | |
| issue | = | 1622, | |
| } | |||
