Automatic Veri.cation of Concurrent Ada Programs
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.
KeywordsProtected Object Translation Step Concurrent Behavior Dine Philosopher Problem Entry Call
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- HL85.D. Helmbold and D. Luckham. Debugging Ada-tasking programs. IEEE Transactions on Software Engineering, Vol. 2(No. 2):45–57, 1985.Google Scholar
- 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
- 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
- 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
- VJKT95.K. Varoaaniemi, Halme J., Hiekanen K., and Pyssisalo T. prod reference manual. Technical Report 13, Helsinki Univ. of Tecnologies, Finland, 1995.Google Scholar