Skip to main content
SpringerLink
Log in

Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules

  • Chapter
Book cover Concurrency, Compositionality, and Correctness

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5930))

Abstract

Starting from the perspective of safety-critical systems development in avionics, railways and the automotive domain, we advocate an integrated verification approach for C/C++ modules combining abstract interpretation, formal verification and conventional testing. It is illustrated how testing and formal verification can benefit from abstract interpretation results and, vice versa, how test automation techniques may help to reduce the well known problem of false alarms frequently encountered in abstract interpretations. As a consequence, verification tools integrating these different methodologies can provide a wider variety of useful results to their users and facilitate the bug localisation processes involved. When applied to C/C++ software, the problems of aliasing, type casts and mixed arithmetic and bit operations have to be handled on the level of constraint generation. We cope with this problem by using a symbolic interpretation method operating on an abstracted memory model. We describe the available tool support developed by the author, his research group and industrial partners.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. IEC 61508 Functional safety of electric/electronic/programmable electronic safety-related systems. International Electrotechnical Commission (2006)

    Google Scholar 

  2. Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (1991)

    Book  MATH  Google Scholar 

  3. Badban, B., Fränzle, M., Peleska, J., Teige, T.: Test automation for hybrid systems. In: Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006), Portland Oregon, USA (November 2006)

    Google Scholar 

  4. Beck, K.: Test-Driven Development. Addison-Wesley, Reading (2003)

    Google Scholar 

  5. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min, A., Monniaux, D., Rival, X.: Combination of abstractions in the Astrée static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008) (to appear)

    Chapter  Google Scholar 

  6. de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  7. Blanchet, B., et al.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. European Committee for Electrotechnical Standardization. EN 50128 – Railway applications – Communications, signalling and processing systems – Software for railway control and protection systems. CENELEC, Brussels (2001)

    Google Scholar 

  9. Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., Rauch, F.: Goanna - a static model checker. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 297–300. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation (2007)

    Google Scholar 

  11. GCC, the GNU Compiler Collection. The GIMPLE family of intermediate representations, http://gcc.gnu.org/wiki/GIMPLE

  12. Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Jaulin, L., Kieffer, M., Didrit, O., Walter, É.: Applied Interval Analysis. Springer, London (2001)

    Book  MATH  Google Scholar 

  14. Leveson, N.G.: Safeware. Addison-Wesley, Reading (1995)

    Google Scholar 

  15. Löding, H.: Behandlung komplexer Datentypen in der automatischen Testdatengenerierung. Master’s thesis, University of Bremen (May 2007)

    Google Scholar 

  16. Peleska, J., Löding, H.: Static Analysis By Abstract Interpretation. University of Bremen, Centre of Information Technology (2008), http://www.informatik.uni-bremen.de/agbs/lehre/ws0708/ai/saai_script.pdf

  17. Peleska, J., Löding, H.: Symbolic and abstract interpretation for c/c++ programs. In: Proceedings of the 3rd intl Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2008)

    Google Scholar 

  18. Peleska, J., Löding, H., Kotas, T.: Test automation meets static analysis. In: Koschke, R., Herzog, K.-H.R.O., Ronthaler, M. (eds.) Proceedings of the INFORMATIK 2007, Band 2, Bremen (Germany), September 24-27, pp. 280–286 (2007)

    Google Scholar 

  19. Peleska, J., Zahlten, C.: Integrated automated test case generation and static analysis. In: Proceedings of the QA+Test 2007 International Conference on QA+Testing Embedded Systems, Bilbao (Spain), October 17-19 (2007)

    Google Scholar 

  20. Ranise, S., Tinelli, C.: Satisfiability modulo theories. TRENDS and CONTROVERSIES–IEEE Magazine on Intelligent Systems 21(6), 71–81 (2006)

    Google Scholar 

  21. SC-167. Software Considerations in Airborne Systems and Equipment Certification. RTCA (1992)

    Google Scholar 

  22. Schlich, B., Salewski, F., Kowalewski, S.: Applying model checking to an automotive microcontroller application. In: Proc. IEEE 2nd Int’l Symp. Industrial Embedded Systems (SIES 2007). IEEE, Los Alamitos (2007)

    Google Scholar 

  23. Strichman, O.: On solving presburger and linear arithmetic with sat. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 160–170. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, p. 115. Consultants Bureau, New York (1962)

    Google Scholar 

  25. Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded c programs. In: Proceedings of the PLDI 2004, Washington, DC, USA, June 9-11. ACM, New York (2004)

    Google Scholar 

  26. Verified Systems International GmbH, Bremen. RT-Tester 6.2 – User Manual (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Bremen, Germany

    Jan Peleska

Authors
  1. Jan Peleska
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Bell Laboratories, 600 Mountain Ave., 07974, Murray Hill, NJ, USA

    Dennis Dams

  2. Computer Science Department, University of Bremen, P.O. Box 330440, 28334, Bremen, Germany

    Ulrich Hannemann

  3. Faculty of Mathematics and Natural Sciences, Department of Computer Science, University of Oslo, P.O. Box 1080, 0316, Blindern, Oslo, Norway

    Martin Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Peleska, J. (2010). Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules. In: Dams, D., Hannemann, U., Steffen, M. (eds) Concurrency, Compositionality, and Correctness. Lecture Notes in Computer Science, vol 5930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11512-7_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11512-7_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11511-0

  • Online ISBN: 978-3-642-11512-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation