Skip to main content
SpringerLink
Log in

Validation of concurrent Ada™ programs using symbolic execution

  • Analysis And Validation
  • Conference paper
  • First Online:
Book cover ESEC '89 (ESEC 1989)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 387))

Included in the following conference series:

Abstract

Symbolic execution is a well known technique for analyzing sequential programs. It has a set of important applications: it can be used for verifying the correctness of a particular path for all the input data which cause the execution of that path. It can support testing tools identifying the constraints that characterize the set of data which exercize a particular execution path. With suitable assertions it can provide a verification mechanism. Finally, it can be used as a basis for a documentation tool.

In this paper we propose an extension of sequential symbolic execution for Ada tasking. A net based formalism, EF net, is used for representing the Ada task system. EF nets are suitable for representing all the aspects of Ada tasking, except for time related commands, which are not considered in this paper. Two symbolic execution algorithms are then defined on EF nets. The first one, called SEA, suitable for the execution of every EF net, can be used for symbolically executing every concurrent Ada program. The second algorithm allows the execution of a relevant subset of EF nets, and improves the SEA algorithm reducing the produced results, dropping some aspects which do not add any significance.

The research activity of Sandro Morasca is supported by Selenia S.p.A..

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. Billington J., Wheeler G. R., Wilbur-Ham M. C., PROTEAN: a High-level Petri Net Tool for the Specification and Verification of Communication Protocol. IEEE Transactions on Software Engineering, vol. SE-14, March 1988.

    Google Scholar 

  2. Bristow G., Drey C., Edwards B., Riddle W., Anomaly Detection in Concurrent Programs, Proceedings of the 4th International Conference on Software Engineering, Munich 1979.

    Google Scholar 

  3. Bruno G., Marchetto G., Process-Translatable Petri Nets for the Rapid Prototyping of Process Control Systems. IEEE Transactions on Software Engineering, vol. SE12, February 1986.

    Google Scholar 

  4. Clarke L. A., A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering, vol. SE2, n. 3, September 76.

    Google Scholar 

  5. Clarke L. A., Richardson D. J., Symbolic Evaluation Method-Implementations and Applications. Proceedings of the Summer School on Computer Program Testing, June, 29th–July, 3rd, 1981, Chandrasekaran and Radicchi eds., North Holland Publishing Company 1981.

    Google Scholar 

  6. Clarke L. A., Richardson D. J., Symbolic Evaluation-an Aid to Testing and Verification. Software Validation, H. Hauser ed., North Holland Publishing Company 1984.

    Google Scholar 

  7. Dillon L. K., Kemmerer R. A., Harrison L. J., An Experience with two Symbolic Execution Based Approaches to Formal Verification of Ada Tasking Programs. Proceedings of the 2nd Workshop on Software Testing, Verification and Analysis. 19–21 July 1988 Banff — Canada. IEEE Press.

    Google Scholar 

  8. Reference Manual for the Ada Programming Language. United States-Department of Defence, ANSI/MIL-STD 1815, January 1983.

    Google Scholar 

  9. Genrich H. J., Net Theory and Application. Information Processing 86., H. J. Kugler ed., Elsevier Science Publisher B. V. (North Holland).

    Google Scholar 

  10. German S. M., Monitoring for Deadlock and Blocking in Ada Tasking, IEEE Transactions on Software Engineering, vol. SE10, n. 6, November 1984.

    Google Scholar 

  11. Ghezzi C., Mandrioli D., Morasca S., Pezzè M., On Introducing Time in Petri Nets. 5th International Workshop on Software Specification and Design, Pittsburgh, 19–20 May 1989.

    Google Scholar 

  12. Ghezzi C., Mandrioli D., Morasca S., Pezzè M., Symbolic Execution of Concurrent Programs Using Petri Nets. to appear in Computer Languages, 1989.

    Google Scholar 

  13. Hantler, King J. C., An Introduction to Proving the Correctness of Programs. Computing Surveys, vol. 8, n.3, September 1976.

    Google Scholar 

  14. Howden W. E., A Survey of Static Analysis Methods. In: Tutorial: Software Testing and Validation Techniques, Miller and Howden (eds), IEEE Computer Society Press, 1988.

    Google Scholar 

  15. Howden W. E., A Survey of Dynamic Analysis Methods. In: Tutorial: Software Testing and Validation Techniques, Miller and Howden (eds), IEEE Computer Society Press, 1988.

    Google Scholar 

  16. Jensen K., Coloured Petri Nets. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, part I, W. Brauer, W. Reisig, G. Rozenberg (eds.), Lecture Notes in Computer Science 254, Berlin, Heidelberg, New York; Springer Verlag 1987.

    Google Scholar 

  17. Kemmerer R. A., Testing Formal Specifications to Detect Design Errors. IEEE Transactions on Software Engineering, vol. SE11, n. 1, January 1985.

    Google Scholar 

  18. Kemmerer R. A., Eckmann S. T., UNISEX: a Unix-based Symbolic Executor for Pascal. Software Practice and Experience, vol. 15, May 1985.

    Google Scholar 

  19. King J. C., Symbolic Execution and Program Testing. Communications of the ACM, vol. 19, n. 7, July 1976.

    Google Scholar 

  20. Mandrioli D., Zicari R., Ghezzi C., Tisato F., Modeling the Ada Task System by Petri Nets. Computer Languages, vol. 10, No. 1, 1985.

    Google Scholar 

  21. Morasca S., Pezzè M., The Rationale of an Environment for Real Time Specifications. Proceedings of Euromicro 89 Workshop on Real-time, June 14th–16th, Como (Italy) IEEE Computer Society Press 1989.

    Google Scholar 

  22. Pezzè M., Un Modello per la Specifica e la Valutazione Simbolica di Sistemi Concorrenti ed in Tempo Reale. Politecnico di Milano — Dipartimento di Elettronica, Ph. D. Thesis (in Italian).

    Google Scholar 

  23. Tai K. C., Obaid E. E., Reproducible Testing of AdaTask Programs. Proceedings of IEEE Second International Conference on Ada Applications and Environments, April 8–10, 1986.

    Google Scholar 

  24. Taylor R. N., A General-Purpose Algorithm for Analyzing Concurrent Programs. Communications of ACM, vol. 26, n. 5, May 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Elettronica, Politecnico di Milano, Piazza Leonardo da Vinci 32, 20133, Milano, Italy

    Sandro Morasca

  2. Cefriel-Politecnico di Milano, Via Emanueli 15, 20126, Milano, Italy

    Mauro Pezzè

Authors
  1. Sandro Morasca
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mauro Pezzè
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

C. Ghezzi J. A. McDermid

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Morasca, S., Pezzè, M. (1989). Validation of concurrent Ada™ programs using symbolic execution. In: Ghezzi, C., McDermid, J.A. (eds) ESEC '89. ESEC 1989. Lecture Notes in Computer Science, vol 387. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51635-2_55

Download citation

  • DOI: https://doi.org/10.1007/3-540-51635-2_55

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51635-4

  • Online ISBN: 978-3-540-46723-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation