Lecture Notes in Computer Science, 2008, Volume 5160/2008, 3-22, DOI: 10.1007/978-3-540-85762-4_2

A Unified Approach to Abstract Interpretation, Formal Verification and Testing of C/C++ Modules

Jan Peleska

View Related Documents

Abstract

In this paper, a unified approach to abstract interpretation, formal verification and testing is described. The approach is applicable for verifying and testing C/C++ functions and methods and complies with the requirements of today’s applicable standards for the development of safety-critical systems in the avionics and railway domains. We give an overview over the techniques required and motivate why an integrated approach is not only desirable from the verification specialists’ perspective, but also from the tool builders’ point of view. Tool support for our approach is available, and it is currently applied in industrial verification projects for railway control systems. All techniques can be adapted to model-based testing in a straightforward way. The objective of this article is to describe the interplay between the methods, techniques and tool components involved; we give references to more comprehensive descriptions of the underlying technical details.

Fulltext Preview

Image of the first page of the fulltext document