Automatic Veri.cation of Concurrent Ada Programs

  • Eric Bruneton
  • Jean-François Pradat-Peyre
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1622)


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 veri.cation of concurrent Ada program properties. The Petri net is automatically produced by a translation step and the veri.cation is automatically performed on the net with classical related techniques. A prototype has been developed and .rst results obtained allow us to think that we will be able in a near future to analyze realistic Ada programs.


Protected Object Translation Step Concurrent Behavior Dine Philosopher Problem Entry Call 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Ber86.
    G. Berthelot. Transformations and decompositions of nets. In Advances in Petri Nets, number 254 in LNCS, pages 359–376. Springer-Verlag, 1986.Google Scholar
  2. BHPP97.
    F. Breant, S. Haddad, and J.F. Pradat-Peyre. Characterizing new reductions by means of language and invariant properties. Technical Report 97-04, Conservatoire National des Arts et Métiers, laboratoire Cedric, 1997.Google Scholar
  3. Had91.
    S. Haddad. A reduction theory for colored nets. In Jensen and Rozenberg, editors, High-level Petri Nets, Theory and Application, LNCS, pages 399–425. Springer-Verlag, 1991.Google Scholar
  4. HL85.
    D. Helmbold and D. Luckham. Debugging Ada-tasking programs. IEEE Transactions on Software Engineering, Vol. 2(No. 2):45–57, 1985.Google Scholar
  5. KPP97.
    C. Kaiser and J.F. Pradat-Peyre. Comparing the reliability provided by tasks or protected objects for implementing a resource allocation service: a case study. In TriAda, St Louis, Missouri, november 1997. ACM SIGAda.Google Scholar
  6. MSS89.
    T. Murata, B. Shenker, and S.M. Shatz. Detection of Ada static deadlocks using Petri nets invariants. IEEE Transactions on Software Engineering, Vol. 15(No. 3):314–326, March 1989.CrossRefGoogle Scholar
  7. MZGT85.
    D. Mandrioli, R. Zicari, C. Ghezzi, and F. Tisato. Modeling the Ada task system by Petri nets. Computer Languages, Vol. 10(NO. 1):43–61, 1985.CrossRefGoogle Scholar
  8. SMMW89.
    S.M. Shatz, K. Mai, D. Moorthi, and J. Woodward. A toolkit for automated support of Ada-tasking analysis. In Proceedings of the 9th Int. Conf. on Distributed Computing Systems, pages 595–602, June 1989.Google Scholar
  9. TSM90.
    S. Tu, S.M. Shatz, and T. Murata. Applying Petri nets reduction to support Ada-tasking deadlock detection. In Proceedings of the 10th IEEE Int. Conf. on Distributed Computing Systems, pages 96–102, Paris, France, June 1990.Google Scholar
  10. VJKT95.
    K. Varoaaniemi, Halme J., Hiekanen K., and Pyssisalo T. prod reference manual. Technical Report 13, Helsinki Univ. of Tecnologies, Finland, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Eric Bruneton
    • 1
  • Jean-François Pradat-Peyre
    • 2
  1. 1.INRIA Rhône-AlpesProjet SiracSpain
  2. 2.Conservatoire National des Arts et MétiersLaboratoire CEDRICSpain

Personalised recommendations