Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
G. Berthelot. Transformations and decompositions of nets. In Advances in Petri Nets, number 254 in LNCS, pages 359–376. Springer-Verlag, 1986.
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.
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.
D. Helmbold and D. Luckham. Debugging Ada-tasking programs. IEEE Transactions on Software Engineering, Vol. 2(No. 2):45–57, 1985.
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.
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.
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.
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.
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.
K. Varoaaniemi, Halme J., Hiekanen K., and Pyssisalo T. prod reference manual. Technical Report 13, Helsinki Univ. of Tecnologies, Finland, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruneton, E., Pradat-Peyre, JF. (1999). Automatic Veri.cation of Concurrent Ada Programs. In: González Harbour, M., de la Puente, J.A. (eds) Reliable Software Technologies — Ada-Europe’ 99. Ada-Europe 1999. Lecture Notes in Computer Science, vol 1622. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48753-0_13
Download citation
DOI: https://doi.org/10.1007/3-540-48753-0_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66093-4
Online ISBN: 978-3-540-48753-1
eBook Packages: Springer Book Archive