×

Integrated and automated abstract interpretation, verification and testing of C/C++ modules. (English) Zbl 1274.68201

Dams, Dennis (ed.) et al., Concurrency, compositionality, and correctness. Essays in honor of Willem-Paul de Roever. Berlin: Springer (ISBN 978-3-642-11511-0/pbk). Lecture Notes in Computer Science 5930, 277-299 (2010).
Summary: 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.
For the entire collection see [Zbl 1183.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

ASTREE; Goanna
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] IEC 61508 Functional safety of electric/electronic/programmable electronic safety-related systems. International Electrotechnical Commission (2006)
[2] Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (1991) · Zbl 0733.68053 · doi:10.1007/978-1-4757-4376-0
[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) · doi:10.1145/1188895.1188902
[4] Beck, K.: Test-Driven Development. Addison-Wesley, Reading (2003)
[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) · Zbl 05252981 · doi:10.1007/978-3-540-77505-8_23
[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) · Zbl 0955.68076 · doi:10.1017/CBO9780511663079
[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) · Zbl 1026.68514 · doi:10.1007/3-540-36377-7_5
[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)
[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) · doi:10.1007/978-3-540-70952-7_20
[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) · Zbl 1144.68371
[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) · Zbl 1111.68506 · doi:10.1007/978-3-540-30579-8_24
[13] Jaulin, L., Kieffer, M., Didrit, O., Walter, É.: Applied Interval Analysis. Springer, London (2001) · doi:10.1007/978-1-4471-0249-6
[14] Leveson, N.G.: Safeware. Addison-Wesley, Reading (1995)
[15] Löding, H.: Behandlung komplexer Datentypen in der automatischen Testdatengenerierung. Master’s thesis, University of Bremen (May 2007)
[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)
[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)
[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)
[20] Ranise, S., Tinelli, C.: Satisfiability modulo theories. TRENDS and CONTROVERSIES–IEEE Magazine on Intelligent Systems 21(6), 71–81 (2006)
[21] SC-167. Software Considerations in Airborne Systems and Equipment Certification. RTCA (1992)
[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)
[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) · Zbl 1019.68592 · doi:10.1007/3-540-36126-X_10
[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)
[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)
[26] Verified Systems International GmbH, Bremen. RT-Tester 6.2 – User Manual (2007)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.